---

Step * of Lemma int-rem-exception

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

---

Latex:

---

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


By

---

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

---

Home Index