proposition: Lemma CRopp_strext : un_op_strext CRasCSetoid CRopp.
proof: Proof. intros x y H. change (CRapartT x y)%CR. apply CR_ap_as_Cauchy_IR_ap_2. apply: un_op_strext_unfolded. 1:stepl (CRasCauchy_IR (-x)%CR); [| now apply eq_symmetric; apply CR_opp_as_Cauchy_IR_opp]. stepr (CRasCauchy_IR (-y)%CR); [| now apply eq_symmetric; apply CR_opp_as_Cauchy_IR_opp]. apply CR_ap_as_Cauchy_IR_ap_1. apply H. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.reals.fast.CRGroupOps CoRN.model.monoids.CRmonoid CoRN.reals.fast.CRcorrect CoRN.tactics.CornTac