---

Step * of Lemma div_mul_cancel

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

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  BLemma  `div\_unique2`
  THEN  Auto
  THEN  Try  ((BLemma  `mul\_bounds\_1a`    THEN  Auto))
  THEN  D  0
  THEN  Auto')

---

Home Index