---

Step * of Lemma le_to_lt_rw

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

---

Latex:

---

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


By

---

Latex:
(Unfold  `guard`  0  THEN  Lemma  `le\_to\_lt`)

---

Home Index