---

Step * of Lemma div_bounds_1

∀[a:ℕ]. ∀[n:ℕ+].  (0 ≤ (a ÷ n))
BY
{ (Auto THEN (D 2 THENA Auto) THEN (D 1 THENA Auto)) }

1
1. a : ℤ
2. a ≥ 0 
3. n : ℤ
4. 0 < n
⊢ 0 ≤ (a ÷ n)

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  (D  2  THENA  Auto)  THEN  (D  1  THENA  Auto))

---

Home Index