---

Step * of Lemma not-gt

∀x,y:ℤ.  uiff(¬(y > x);x ≥ y )
BY
{ (RepUR ``ge gt less_than le`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}x,y:\mBbbZ{}.    uiff(\mneg{}(y  >  x);x  \mgeq{}  y  )


By

---

Latex:
(RepUR  ``ge  gt  less\_than  le``  0  THEN  Auto)

---

Home Index