---

Step * of Lemma int-between

∀i,j:ℤ.  ∃k:ℤ. ((i ≤ k) ∧ k < j) supposing i < j
BY
{ (Auto
   THEN (InstLemma `div_rem_sum` [⌜j - i⌝;⌜2⌝]⋅ THENA Auto)
   THEN (InstLemma `rem_bounds_1` [⌜j - i⌝;⌜2⌝]⋅ THENA Auto)
   THEN With ⌜i + ((j - i) ÷ 2)⌝ (D 0)⋅
   THEN Auto') }

---

Latex:

---

Latex:
\mforall{}i,j:\mBbbZ{}.    \mexists{}k:\mBbbZ{}.  ((i  \mleq{}  k)  \mwedge{}  k  <  j)  supposing  i  <  j


By

---

Latex:
(Auto
  THEN  (InstLemma  `div\_rem\_sum`  [\mkleeneopen{}j  -  i\mkleeneclose{};\mkleeneopen{}2\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `rem\_bounds\_1`  [\mkleeneopen{}j  -  i\mkleeneclose{};\mkleeneopen{}2\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  With  \mkleeneopen{}i  +  ((j  -  i)  \mdiv{}  2)\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto')

---

Home Index