---

Step * of Lemma add_mono_wrt_eq_rw

∀[a,b,n:ℤ].  {uiff(a = b ∈ ℤ;(a + n) = (b + n) ∈ ℤ)}
BY
{ (Unfold `guard` 0 THEN Lemma `add_mono_wrt_eq`) }

---

Latex:

---

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


By

---

Latex:
(Unfold  `guard`  0  THEN  Lemma  `add\_mono\_wrt\_eq`)

---

Home Index