---

Step * of Lemma add-comm

∀x,y:ℤ.  ((x + y) = (y + x) ∈ ℤ)
BY
{ ((UnivCD THENA Auto) THEN Refine_addCommutative THEN Fold `member` 0 THEN Declaration) }

---

Latex:

---

Latex:
\mforall{}x,y:\mBbbZ{}.    ((x  +  y)  =  (y  +  x))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  Refine\_addCommutative  THEN  Fold  `member`  0  THEN  Declaration)

---

Home Index