---

Step * of Lemma absval_pos

∀[i:ℕ]. (|i| = i ∈ ℤ)
BY
{ (Auto THEN RWO "absval_unfold" 0 THEN Auto THEN AutoSplit THEN Auto') }

---

Latex:

---

Latex:
\mforall{}[i:\mBbbN{}].  (|i|  =  i)


By

---

Latex:
(Auto  THEN  RWO  "absval\_unfold"  0  THEN  Auto  THEN  AutoSplit  THEN  Auto')

---

Home Index