---

Step * of Lemma assert-qpositive

No Annotations
∀[r:ℚ]. uiff(↑qpositive(r);0 < r)
BY
{ ((D 0 THENA Auto) THEN QArithOps ``qless qadd qmul`` THEN (RW IntNormC 0 THENA Auto) THEN RepeatFor 2 (AutoSplit')) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[r:\mBbbQ{}].  uiff(\muparrow{}qpositive(r);0  <  r)


By

---

Latex:
((D  0  THENA  Auto)
  THEN  QArithOps  ``qless  qadd  qmul``
  THEN  (RW  IntNormC  0  THENA  Auto)
  THEN  RepeatFor  2  (AutoSplit'))

---

Home Index