---

Step * of Lemma ml-absval-sq

∀[x:ℤ]. (ml-absval(x) ~ |x|)
BY
{ ((RepUR ``ml-absval ml_apply absval`` 0 THEN Auto) THEN CallByValueReduce 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[x:\mBbbZ{}].  (ml-absval(x)  \msim{}  |x|)


By

---

Latex:
((RepUR  ``ml-absval  ml\_apply  absval``  0  THEN  Auto)  THEN  CallByValueReduce  0  THEN  Auto)

---

Home Index