---

Step * 1 1 1 1 of Lemma div_bounds_1


1. a : ℤ
2. a ≥ 0 
3. n : ℤ
4. 0 < n
5. a = ((n * (a ÷ n)) + (a rem n)) ∈ ℤ
6. 0 ≤ (a rem n)
7. a rem n < n
8. ¬(0 ≤ (a ÷ n))
9. (n * (a ÷ n)) ≤ ((-1) * n)
10. a ≤ (((-1) * n) + (a rem n))
⊢ 0 ≤ (a ÷ n)
BY
{ ((Assert 0 ≤ (((-1) * n) + (a rem n)) BY Auto) THEN (Add ⌜n⌝ (-1)⋅ THENA Auto) THEN RW IntNormC (-1) THEN Auto) }

---

Latex:

---

Latex:

1.  a  :  \mBbbZ{}
2.  a  \mgeq{}  0 
3.  n  :  \mBbbZ{}
4.  0  <  n
5.  a  =  ((n  *  (a  \mdiv{}  n))  +  (a  rem  n))
6.  0  \mleq{}  (a  rem  n)
7.  a  rem  n  <  n
8.  \mneg{}(0  \mleq{}  (a  \mdiv{}  n))
9.  (n  *  (a  \mdiv{}  n))  \mleq{}  ((-1)  *  n)
10.  a  \mleq{}  (((-1)  *  n)  +  (a  rem  n))
\mvdash{}  0  \mleq{}  (a  \mdiv{}  n)


By

---

Latex:
((Assert  0  \mleq{}  (((-1)  *  n)  +  (a  rem  n))  BY
                Auto)
  THEN  (Add  \mkleeneopen{}n\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto)
  THEN  RW  IntNormC  (-1)
  THEN  Auto)

---

Home Index