---

Step * of Lemma div_bounds_3

∀[a:{...0}]. ∀[n:{...-1}].  (0 ≤ (a ÷ n))
BY
{ (Auto THEN (D 2 THENA Auto) THEN (D 1 THENA Auto) THEN (Assert a rem n ∈ ℤ BY Auto) THEN (Assert a ÷ n ∈ ℤ BY Auto)) }

1
1. a : ℤ
2. a ≤ 0
3. n : ℤ
4. n ≤ (-1)
5. a rem n ∈ ℤ
6. a ÷ n ∈ ℤ
⊢ 0 ≤ (a ÷ n)

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  (D  2  THENA  Auto)
  THEN  (D  1  THENA  Auto)
  THEN  (Assert  a  rem  n  \mmember{}  \mBbbZ{}  BY
                          Auto)
  THEN  (Assert  a  \mdiv{}  n  \mmember{}  \mBbbZ{}  BY
                          Auto))

---

Home Index