---

Step * of Lemma add_cancel_in_eq

∀[a,b,n:ℤ].  a = b ∈ ℤ supposing (a + n) = (b + n) ∈ ℤ
BY
{ Auto }

1
1. a : ℤ
2. b : ℤ
3. n : ℤ
4. (a + n) = (b + n) ∈ ℤ
⊢ a = b ∈ ℤ

---

Latex:

---

Latex:
\mforall{}[a,b,n:\mBbbZ{}].    a  =  b  supposing  (a  +  n)  =  (b  +  n)


By

---

Latex:
Auto

---

Home Index