---

Step * of Lemma add-plus-1-div-2-implies-lt

∀[n,m:ℕ].  n < m supposing n < ((n + m) + 1) ÷ 2
BY
{ ((Auto THEN (Assert (n + 1) ≤ (((n + m) + 1) ÷ 2) BY Auto))
   THEN Mul ⌜2⌝ (-1)⋅
   THEN (Subst' 2 * (((n + m) + 1) ÷ 2) ~ ((n + m) + 1) - (n + m) + 1 rem 2 -1 THENA Auto)
   THEN Assert ⌜0 ≤ ((n + m) + 1 rem 2)⌝⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[n,m:\mBbbN{}].    n  <  m  supposing  n  <  ((n  +  m)  +  1)  \mdiv{}  2


By

---

Latex:
((Auto  THEN  (Assert  (n  +  1)  \mleq{}  (((n  +  m)  +  1)  \mdiv{}  2)  BY  Auto))
  THEN  Mul  \mkleeneopen{}2\mkleeneclose{}  (-1)\mcdot{}
  THEN  (Subst'  2  *  (((n  +  m)  +  1)  \mdiv{}  2)  \msim{}  ((n  +  m)  +  1)  -  (n  +  m)  +  1  rem  2  -1  THENA  Auto)
  THEN  Assert  \mkleeneopen{}0  \mleq{}  ((n  +  m)  +  1  rem  2)\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index