---

Step * of Lemma absval-as-imax

∀[a:ℤ]. (imax(a;-a) = |a| ∈ ℤ)
BY
{ ((UnivCD THENA Auto) THEN RWO "absval_unfold imax_unfold" 0 THEN Repeat (AutoSplit) THEN Auto') }

---

Latex:

---

Latex:
\mforall{}[a:\mBbbZ{}].  (imax(a;-a)  =  |a|)


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  RWO  "absval\_unfold  imax\_unfold"  0  THEN  Repeat  (AutoSplit)  THEN  Auto')

---

Home Index