---

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 * 2 < (((n + m) + 1) ÷ 2) * 2⌝⋅ THENA Auto')
   THEN (Subst ⌜((((n + m) + 1) ÷ 2) * 2) = (((n + m) + 1) - (n + m) + 1 rem 2) ∈ ℤ⌝ (-1)⋅
         THENA (Auto
                THEN Assert ⌜((n + m) + 1) = (((((n + m) + 1) ÷ 2) * 2) + ((n + m) + 1 rem 2)) ∈ ℤ⌝⋅
                THEN Auto'
                THEN BLemma `div_rem_sum`
                THEN Auto)
         )
   THEN (Assert ⌜((n * 2) - n - 1) + ((n + m) + 1 rem 2) < m⌝⋅ THENA Auto')
   THEN (Subst ⌜((n * 2) - n) = n ∈ ℤ⌝ (-1)⋅ THENA Auto')
   THEN (InstLemma `rem_bounds_1` [⌜(n + m) + 1⌝;⌜2⌝]⋅ THENA Auto')
   THEN RepD
   THEN (Assert ⌜(((n + m) + 1 rem 2) = 0 ∈ ℤ) ∨ (((n + m) + 1 rem 2) = 1 ∈ ℤ)⌝⋅ THENA Auto')
   THEN RepeatFor 2 (Thin (-2))
   THEN D (-1)
   THEN Auto'
   THEN Duplicate (-1)
   THEN (RWO "rem_add1" (-1) THENA Auto')) }

1
1. n : ℕ
2. m : ℕ
3. n < ((n + m) + 1) ÷ 2
4. n * 2 < ((n + m) + 1) - (n + m) + 1 rem 2
5. (n - 1) + ((n + m) + 1 rem 2) < m
6. ((n + m) + 1 rem 2) = 0 ∈ ℤ
7. if (n + m rem 2 =z 2 - 1) then 0 else (n + m rem 2) + 1 fi  = 0 ∈ ℤ
⊢ n < m

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  (Assert  \mkleeneopen{}n  *  2  <  (((n  +  m)  +  1)  \mdiv{}  2)  *  2\mkleeneclose{}\mcdot{}  THENA  Auto')
  THEN  (Subst  \mkleeneopen{}((((n  +  m)  +  1)  \mdiv{}  2)  *  2)  =  (((n  +  m)  +  1)  -  (n  +  m)  +  1  rem  2)\mkleeneclose{}  (-1)\mcdot{}
              THENA  (Auto
                            THEN  Assert  \mkleeneopen{}((n  +  m)  +  1)  =  (((((n  +  m)  +  1)  \mdiv{}  2)  *  2)  +  ((n  +  m)  +  1  rem  2))\mkleeneclose{}\mcdot{}
                            THEN  Auto'
                            THEN  BLemma  `div\_rem\_sum`
                            THEN  Auto)
              )
  THEN  (Assert  \mkleeneopen{}((n  *  2)  -  n  -  1)  +  ((n  +  m)  +  1  rem  2)  <  m\mkleeneclose{}\mcdot{}  THENA  Auto')
  THEN  (Subst  \mkleeneopen{}((n  *  2)  -  n)  =  n\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto')
  THEN  (InstLemma  `rem\_bounds\_1`  [\mkleeneopen{}(n  +  m)  +  1\mkleeneclose{};\mkleeneopen{}2\mkleeneclose{}]\mcdot{}  THENA  Auto')
  THEN  RepD
  THEN  (Assert  \mkleeneopen{}(((n  +  m)  +  1  rem  2)  =  0)  \mvee{}  (((n  +  m)  +  1  rem  2)  =  1)\mkleeneclose{}\mcdot{}  THENA  Auto')
  THEN  RepeatFor  2  (Thin  (-2))
  THEN  D  (-1)
  THEN  Auto'
  THEN  Duplicate  (-1)
  THEN  (RWO  "rem\_add1"  (-1)  THENA  Auto'))

---

Home Index