---

Step * of Lemma add_mono_wrt_le_rw

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

---

Latex:

---

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


By

---

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

---

Home Index