---

Step * of Lemma div_bounds_4

∀[a:{...0}]. ∀[n:{...-1}].  (0 ≤ (a ÷ n))
BY
{ ((Auto THEN (InstLemma `div_rem_sum` [⌜a⌝;⌜n⌝]⋅ THENA Auto))
   THEN Auto
   THEN (InstLemma `rem_bounds_3` [⌜a⌝;⌜n⌝]⋅ THENA Auto)
   THEN SupposeNot) }

---

Latex:

---

Latex:
\mforall{}[a:\{...0\}].  \mforall{}[n:\{...-1\}].    (0  \mleq{}  (a  \mdiv{}  n))


By

---

Latex:
((Auto  THEN  (InstLemma  `div\_rem\_sum`  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THENA  Auto))
  THEN  Auto
  THEN  (InstLemma  `rem\_bounds\_3`  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  SupposeNot)

---

Home Index