---

Step * of Lemma lt_to_le_rw

∀[i,j:ℤ].  {uiff(i < j;(i + 1) ≤ j)}
BY
{ (Unfold `guard` 0 THEN Lemma `lt_to_le`) }

---

Latex:

---

Latex:
\mforall{}[i,j:\mBbbZ{}].    \{uiff(i  <  j;(i  +  1)  \mleq{}  j)\}


By

---

Latex:
(Unfold  `guard`  0  THEN  Lemma  `lt\_to\_le`)

---

Home Index