---

Step * of Lemma minus-add

∀[x,y:Top].  (-(x + y) ~ (-x) + (-y))
BY
{ TACTIC:Assert ⌜∀x,y:ℤ.  ((-(x + y)) = ((-x) + (-y)) ∈ ℤ)⌝⋅ }

1
.....assertion..... 
∀x,y:ℤ.  ((-(x + y)) = ((-x) + (-y)) ∈ ℤ)

2
1. ∀x,y:ℤ.  ((-(x + y)) = ((-x) + (-y)) ∈ ℤ)
⊢ ∀[x,y:Top].  (-(x + y) ~ (-x) + (-y))

---

Latex:

---

Latex:
\mforall{}[x,y:Top].    (-(x  +  y)  \msim{}  (-x)  +  (-y))


By

---

Latex:
TACTIC:Assert  \mkleeneopen{}\mforall{}x,y:\mBbbZ{}.    ((-(x  +  y))  =  ((-x)  +  (-y)))\mkleeneclose{}\mcdot{}

---

Home Index