---

Step * 1 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 < m
6. ((n + m) + 1 rem 2) = 0 ∈ ℤ
7. (n + m rem 2) = 1 ∈ ℤ
8. ↑isOdd(n + m)
⊢ n < m
BY
{ ((FLemma `isOdd-add` [-1] THENA Auto)
   THEN (FLemma `not-same-parity-implies-even-odd` [-1] THENA Auto)
   THEN (Assert ⌜n < m ∨ (n = m ∈ ℤ)⌝⋅ THENA Auto)
   THEN D (-1)
   THEN Auto
   THEN (Assert ⌜False⌝⋅ THEN Auto)
   THEN D (-2)
   THEN RepD
   THEN Try (Complete ((FLemma `even-iff-not-odd` [-3] THEN Auto)))
   THEN Try (Complete ((FLemma `even-iff-not-odd` [-2] THEN Auto))))⋅ }

---

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  <  m
6.  ((n  +  m)  +  1  rem  2)  =  0
7.  (n  +  m  rem  2)  =  1
8.  \muparrow{}isOdd(n  +  m)
\mvdash{}  n  <  m


By

---

Latex:
((FLemma  `isOdd-add`  [-1]  THENA  Auto)
  THEN  (FLemma  `not-same-parity-implies-even-odd`  [-1]  THENA  Auto)
  THEN  (Assert  \mkleeneopen{}n  <  m  \mvee{}  (n  =  m)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  D  (-1)
  THEN  Auto
  THEN  (Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto)
  THEN  D  (-2)
  THEN  RepD
  THEN  Try  (Complete  ((FLemma  `even-iff-not-odd`  [-3]  THEN  Auto)))
  THEN  Try  (Complete  ((FLemma  `even-iff-not-odd`  [-2]  THEN  Auto))))\mcdot{}

---

Home Index