---

Step * of Lemma lt_int_eq_false_elim

∀[i,j:ℤ].  ¬i < j supposing i <z j = ff
BY
{ (UnivCD THENA Auto) }

1
1. i : ℤ
2. j : ℤ
3. i <z j = ff
⊢ ¬i < j

---

Latex:

---

Latex:
\mforall{}[i,j:\mBbbZ{}].    \mneg{}i  <  j  supposing  i  <z  j  =  ff


By

---

Latex:
(UnivCD  THENA  Auto)

---

Home Index