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