---

Step * of Lemma neg_assoced

∀a:ℤ. ((-a) ~ a)
BY
{ ((Unfold `assoced` 0 THENM GenRepD) THENA Auto) }

1
1. a : ℤ
⊢ (-a) | a

2
1. a : ℤ
⊢ a | (-a)

---

Latex:

---

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


By

---

Latex:
((Unfold  `assoced`  0  THENM  GenRepD)  THENA  Auto)

---

Home Index