proposition: Lemma IR_div_as_CR : forall x y y_ y__, (IRasCR (x[/]y[//]y_) == IRasCR x * CRinvT (IRasCR y) y__)%CR.
proof: Proof. intros x y y_ y__. apply (@mult_cancel_lft CRasCField _ _ (IRasCR y)). apply (map_pres_ap_zero _ _ (iso_map_rht _ _ CRIR_iso) y y_). rewrite <- IR_mult_as_CR. transitivity (IRasCR x). apply IRasCR_wd; rational. simpl. rewrite (CRmult_comm (IRasCR x)), <- CRmult_assoc, CRmult_inv_r. rewrite CRmult_1_l. reflexivity. 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