proposition: Lemma IR_recip_as_CR :forall y y_ y__, (IRasCR ([1][/]y[//]y_)==(CRinvT (IRasCR y) y__))%CR.
proof: Proof. intros y y_ y__. assert (X:=(IR_div_as_CR [1] y y_ y__)). rewrite -> X. change ((IRasCR [1] * CRinvT (IRasCR y) y__) == (CRinvT (IRasCR y) y__))%CR. rewrite -> IR_One_as_CR. change ((1 * CRinvT (IRasCR y) y__ == CRinvT (IRasCR y) y__)%CR). ring. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.reals.CauchySeq CoRN.reals.iso_CReals CoRN.reals.R_morphism CoRN.reals.fast.CRArith CoRN.model.reals.CRreal CoRN.tactics.CornTac