---

Step * of Lemma div-cancel

∀[x:ℤ]. ∀[y:ℤ-o].  ((x * y) ÷ y ~ x)
BY
{ (Auto THEN BLemma `div_unique3`  THEN Auto THEN InstConcl [⌜0⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[x:\mBbbZ{}].  \mforall{}[y:\mBbbZ{}\msupminus{}\msupzero{}].    ((x  *  y)  \mdiv{}  y  \msim{}  x)


By

---

Latex:
(Auto  THEN  BLemma  `div\_unique3`    THEN  Auto  THEN  InstConcl  [\mkleeneopen{}0\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index