proposition: Lemma CRinv_strext : forall x y x_ y_, CRapartT (CRinvT x x_) (CRinvT y y_) -> CRapartT x y.
proof: Proof. intros x y x_ y_ H. apply CR_ap_as_Cauchy_IR_ap_2. apply cf_rcpsx with (CR_nonZero_as_Cauchy_IR_nonZero_1 _ x_) (CR_nonZero_as_Cauchy_IR_nonZero_1 _ y_). stepl (CRasCauchy_IR (CRinvT x x_)%CR); [| now apply eq_symmetric; apply (CR_inv_as_Cauchy_IR_inv_short x x_)]. stepr (CRasCauchy_IR (CRinvT y y_)%CR); [| now apply eq_symmetric; apply (CR_inv_as_Cauchy_IR_inv_short y y_)]. apply CR_ap_as_Cauchy_IR_ap_1. apply H. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.reals.fast.CRFieldOps CoRN.model.rings.CRring CoRN.algebra.CFields CoRN.reals.fast.CRcorrect CoRN.tactics.CornTac