---

Step * of Lemma zero-qle-qabs

∀[r:ℚ]. (0 ≤ |r|)
BY
{ xxx(xxxAutoxxx THEN Unfold `qabs` 0 THEN (CallByValueReduce 0 THENA Auto) THEN AutoBoolCase qpositive(r)⋅)xxx }

1
1. r : ℚ
2. ¬0 < r
⊢ 0 ≤ -(r)

---

Latex:

---

Latex:
\mforall{}[r:\mBbbQ{}].  (0  \mleq{}  |r|)


By

---

Latex:
xxx(xxxAutoxxx
        THEN  Unfold  `qabs`  0
        THEN  (CallByValueReduce  0  THENA  Auto)
        THEN  AutoBoolCase  qpositive(r)\mcdot{})xxx

---

Home Index