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