---

Step * 1 of Lemma not-le-2


1. x : ℤ@i
2. y : ℤ@i
⊢ uiff((1 + y) ≤ x;(y + 1) ≤ x)
BY
{ Auto }

---

Latex:

---

Latex:

1.  x  :  \mBbbZ{}@i
2.  y  :  \mBbbZ{}@i
\mvdash{}  uiff((1  +  y)  \mleq{}  x;(y  +  1)  \mleq{}  x)


By

---

Latex:
Auto

---

Home Index