---

Step * 1 1 of Lemma rless-int


1. n : ℤ@i
2. m : ℤ@i
3. k : ℕ+@i
4. (2 * k * n) + 4 < 2 * k * m@i
⊢ n < m
BY
{ (SupposeNot THEN (Assert m ≤ n BY Auto) THEN Mul ⌜2 * k⌝ (-1)⋅ THEN Auto') }

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}@i
2.  m  :  \mBbbZ{}@i
3.  k  :  \mBbbN{}\msupplus{}@i
4.  (2  *  k  *  n)  +  4  <  2  *  k  *  m@i
\mvdash{}  n  <  m


By

---

Latex:
(SupposeNot  THEN  (Assert  m  \mleq{}  n  BY  Auto)  THEN  Mul  \mkleeneopen{}2  *  k\mkleeneclose{}  (-1)\mcdot{}  THEN  Auto')

---

Home Index