---

Step * of Lemma lt_int_eq_false_elim_sqequal

∀[i,j:ℤ].  ¬i < j supposing i <z j ~ ff
BY
{ (Auto THEN Assert ⌜¬↑i <z j⌝⋅ THEN Try ((RW assert_pushdownC (-1) THEN Auto))) }

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  Assert  \mkleeneopen{}\mneg{}\muparrow{}i  <z  j\mkleeneclose{}\mcdot{}  THEN  Try  ((RW  assert\_pushdownC  (-1)  THEN  Auto)))

---

Home Index