---

Step * of Lemma int-div-exception

∀[x:ℤ]. ∀[u,v:Top].  (x ÷ exception(u; v) ~ exception(u; v))
BY
{ TACTIC:((UnivCD THENA Auto) THEN Refine_exceptionDivide THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[x:\mBbbZ{}].  \mforall{}[u,v:Top].    (x  \mdiv{}  exception(u;  v)  \msim{}  exception(u;  v))


By

---

Latex:
TACTIC:((UnivCD  THENA  Auto)  THEN  Refine\_exceptionDivide  THEN  Auto)

---

Home Index