---

Step * of Lemma absval_assoced

∀a:ℤ. (|a| ~ a)
BY
{ (((RepD THENM RWO "absval_unfold" 0) THENA Auto) THEN AutoSplit) }

1
1. a : ℤ
2. -1 < a
⊢ a ~ a

---

Latex:

---

Latex:
\mforall{}a:\mBbbZ{}.  (|a|  \msim{}  a)


By

---

Latex:
(((RepD  THENM  RWO  "absval\_unfold"  0)  THENA  Auto)  THEN  AutoSplit)

---

Home Index