---

Step * of Lemma add_mono_wrt_eq

∀[a,b,n:ℤ].  uiff(a = b ∈ ℤ;(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{}].    uiff(a  =  b;(a  +  n)  =  (b  +  n))


By

---

Latex:
Auto

---

Home Index