---

Step * of Lemma div-cancel2

∀[x:ℤ]. ∀[y:ℤ-o].  ((y * x) ÷ y ~ x)
BY
{ ((UnivCD THENA Auto) THEN (Subst' y * x ~ x * y 0 THENA Auto) THEN BLemma `div-cancel` THEN Auto) }

---

Latex:

---

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


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  (Subst'  y  *  x  \msim{}  x  *  y  0  THENA  Auto)  THEN  BLemma  `div-cancel`  THEN  Auto)

---

Home Index