---

Step * of Lemma qless-minus

No Annotations
∀[a,b:ℚ].  uiff(a < b;-(b) < -(a))
BY
{ (RepeatFor 2 ((D 0 THENA Auto))
   THEN RepUR ``qless grp_lt oset_of_ocmon dset_of_mon set_lt set_blt q_le`` 0
   THEN RepeatFor 2 ((CallByValueReduce 0 THENA Auto))) }

1
1. a : ℚ
2. b : ℚ
⊢ uiff(↑((qpositive(b - a) ∨bqeq(a;b)) ∧b (¬b(qpositive(a - b) ∨bqeq(b;a))));↑((qpositive(-(a) - -(b)) ∨bqeq(-(b);-(a)))
∧b (¬b(qpositive(-(b) - -(a)) ∨bqeq(-(a);-(b))))))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[a,b:\mBbbQ{}].    uiff(a  <  b;-(b)  <  -(a))


By

---

Latex:
(RepeatFor  2  ((D  0  THENA  Auto))
  THEN  RepUR  ``qless  grp\_lt  oset\_of\_ocmon  dset\_of\_mon  set\_lt  set\_blt  q\_le``  0
  THEN  RepeatFor  2  ((CallByValueReduce  0  THENA  Auto)))

---

Home Index