---

Step * of Lemma div_bounds_2

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

1
1. a : {...-1}
2. n : ℕ+
3. a = (((a ÷ n) * n) + (a rem n)) ∈ ℤ
4. (0 ≥ (a rem n) ) ∧ ((a rem n) > (-n))
⊢ (a ÷ n) ≤ 0

---

Latex:

---

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


By

---

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

---

Home Index