---

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


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
BY
{ ((SplitOnHypITE (-1) THENA Auto)
   THEN Try (Complete ((Assert ⌜0 ≤ (n + m rem 2)⌝⋅
                        THEN Auto'
                        THEN InstLemma `rem_bounds_1` [⌜n + m⌝;⌜2⌝]⋅
                        THEN Auto')))
   THEN Reduce (-1)
   THEN (Thin (-2)
         THEN HypSubst' (-2) (-3)
         THEN (Subst ⌜(n - 1) + 0 ~ n - 1⌝ (-3)⋅ THENA Auto)
         THEN (Assert ⌜↑isOdd(n + m)⌝⋅
               THENA (RepUR ``isOdd`` 0 THEN AllPushDown THEN RepUR ``modulus`` 0 THEN AutoSplit THEN 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 < m
6. ((n + m) + 1 rem 2) = 0 ∈ ℤ
7. (n + m rem 2) = 1 ∈ ℤ
8. ↑isOdd(n + m)
⊢ n < m

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  m  :  \mBbbN{}
3.  n  <  ((n  +  m)  +  1)  \mdiv{}  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  =\msubz{}  2  -  1)  then  0  else  (n  +  m  rem  2)  +  1  fi    =  0
\mvdash{}  n  <  m


By

---

Latex:
((SplitOnHypITE  (-1)  THENA  Auto)
  THEN  Try  (Complete  ((Assert  \mkleeneopen{}0  \mleq{}  (n  +  m  rem  2)\mkleeneclose{}\mcdot{}
                                            THEN  Auto'
                                            THEN  InstLemma  `rem\_bounds\_1`  [\mkleeneopen{}n  +  m\mkleeneclose{};\mkleeneopen{}2\mkleeneclose{}]\mcdot{}
                                            THEN  Auto')))
  THEN  Reduce  (-1)
  THEN  (Thin  (-2)
              THEN  HypSubst'  (-2)  (-3)
              THEN  (Subst  \mkleeneopen{}(n  -  1)  +  0  \msim{}  n  -  1\mkleeneclose{}  (-3)\mcdot{}  THENA  Auto)
              THEN  (Assert  \mkleeneopen{}\muparrow{}isOdd(n  +  m)\mkleeneclose{}\mcdot{}
                          THENA  (RepUR  ``isOdd``  0
                                        THEN  AllPushDown
                                        THEN  RepUR  ``modulus``  0
                                        THEN  AutoSplit
                                        THEN  Auto')
                          ))\mcdot{})

---

Home Index