---

Step * of Lemma absval-non-neg

∀[x:ℤ]. (0 ≤ |x|)
BY
{ ((UnivCD THENA Auto) THEN Decide x = 0 ∈ ℤ THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[x:\mBbbZ{}].  (0  \mleq{}  |x|)


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  Decide  x  =  0  THEN  Auto)

---

Home Index