---

Step * of Lemma add-inverse

∀[x:ℤ]. (x + (-x) ~ 0)
BY
{ TACTIC:((UnivCD THENA Auto)
          THEN (Assert (x + (-x)) = 0 ∈ ℤ BY
                      (Refine_addInverse THEN Fold `member` 0 THEN Declaration))
          ) }

1
1. x : ℤ
2. (x + (-x)) = 0 ∈ ℤ
⊢ x + (-x) ~ 0

---

Latex:

---

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


By

---

Latex:
TACTIC:((UnivCD  THENA  Auto)
                THEN  (Assert  (x  +  (-x))  =  0  BY
                                        (Refine\_addInverse  THEN  Fold  `member`  0  THEN  Declaration))
                )

---

Home Index