---

Step * of Lemma div_mul_add_cancel

∀[a:ℕ]. ∀[b:ℕ+]. ∀[r:ℕb].  ((((a * b) + r) ÷ b) = a ∈ ℤ)
BY
{ (Auto
   THEN BLemma `div_unique2`
   THEN Auto
   THEN (Assert 0 ≤ (a * b) BY
               (BLemma `mul_bounds_1a`  THEN Auto))
   THEN Auto'
   THEN D 0
   THEN Auto') }

---

Latex:

---

Latex:
\mforall{}[a:\mBbbN{}].  \mforall{}[b:\mBbbN{}\msupplus{}].  \mforall{}[r:\mBbbN{}b].    ((((a  *  b)  +  r)  \mdiv{}  b)  =  a)


By

---

Latex:
(Auto
  THEN  BLemma  `div\_unique2`
  THEN  Auto
  THEN  (Assert  0  \mleq{}  (a  *  b)  BY
                          (BLemma  `mul\_bounds\_1a`    THEN  Auto))
  THEN  Auto'
  THEN  D  0
  THEN  Auto')

---

Home Index