---

Step * of Lemma add-zero

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

---

Latex:

---

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


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  (RWO  "add-commutes"  0  THENA  Trivial)  THEN  RWO  "zero-add"  0  THEN  Trivial)

---

Home Index