---

Step * of Lemma minus-minus-sq

∀x:Top. (--x ~ x + 0)
BY
{ ((Intros THEN SqEqualTopToBase) THEN SqReasoning) }

1
1. x : Base
2. (--x)↓
3. -x ∈ ℤ
4. (-x)↓
5. x ∈ ℤ
⊢ --x ≤ x + 0

---

Latex:

---

Latex:
\mforall{}x:Top.  (--x  \msim{}  x  +  0)


By

---

Latex:
((Intros  THEN  SqEqualTopToBase)  THEN  SqReasoning)

---

Home Index