---

Step * of Lemma add-inverse2

∀[x:ℤ]. ((-x) + x ~ 0)
BY
{ ((UnivCD THENA Auto) THEN (RWO "add-commutes" 0 THENA Auto) THEN (BLemma `add-inverse` THENA Auto)) }

---

Latex:

---

Latex:
\mforall{}[x:\mBbbZ{}].  ((-x)  +  x  \msim{}  0)


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  (RWO  "add-commutes"  0  THENA  Auto)  THEN  (BLemma  `add-inverse`  THENA  Auto))

---

Home Index