---

Step * of Lemma not-le-2

∀x,y:ℤ.  uiff(¬(x ≤ y);(y + 1) ≤ x)
BY
{ ((UnivCD THENA Auto) THEN (RWO "not-le" 0 THENA Auto) THEN (RWO "less-iff-le" 0 THENA Auto)) }

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

---

Latex:

---

Latex:
\mforall{}x,y:\mBbbZ{}.    uiff(\mneg{}(x  \mleq{}  y);(y  +  1)  \mleq{}  x)


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  (RWO  "not-le"  0  THENA  Auto)  THEN  (RWO  "less-iff-le"  0  THENA  Auto))

---

Home Index