---

Step * of Lemma qabs-nonneg

∀[r:ℚ]. (0 ≤ |r|)
BY
{ (Auto THEN (Unfold `qabs` 0 THEN (CallByValueReduce 0 THENA Auto)) THEN AutoSplit THEN Try ((RelRST THEN Auto))) }

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  (Unfold  `qabs`  0  THEN  (CallByValueReduce  0  THENA  Auto))
  THEN  AutoSplit
  THEN  Try  ((RelRST  THEN  Auto)))

---

Home Index