---

Step * of Lemma qminus-positive

∀[r:ℚ]. uiff(0 < -(r);r < 0)
BY
{ (Auto THEN Try ((QAdd ⌜r⌝ 0⋅ THEN Complete (Auto))) THEN Try ((QAdd ⌜r⌝ (-1)⋅ THEN Complete (Auto)))) }

---

Latex:

---

Latex:
\mforall{}[r:\mBbbQ{}].  uiff(0  <  -(r);r  <  0)


By

---

Latex:
(Auto
  THEN  Try  ((QAdd  \mkleeneopen{}r\mkleeneclose{}  0\mcdot{}  THEN  Complete  (Auto)))
  THEN  Try  ((QAdd  \mkleeneopen{}r\mkleeneclose{}  (-1)\mcdot{}  THEN  Complete  (Auto))))

---

Home Index