proposition: Lemma CRplus_strext : bin_op_strext CRasCSetoid (ucFun2 CRplus_uc).
proof: Proof. intros x1 x2 y1 y2 H. simpl in *. assert (X:(CRasCauchy_IR x1[+]CRasCauchy_IR y1)[#](CRasCauchy_IR x2[+]CRasCauchy_IR y2)). stepl (CRasCauchy_IR (x1+y1)%CR); [| apply eq_symmetric; apply CR_plus_as_Cauchy_IR_plus]. stepr (CRasCauchy_IR (x2+y2)%CR); [| now apply eq_symmetric; apply CR_plus_as_Cauchy_IR_plus]. apply CR_ap_as_Cauchy_IR_ap_1. assumption. destruct (bin_op_strext_unfolded _ _ _ _ _ _ X);[left|right]; apply CR_ap_as_Cauchy_IR_ap_2; assumption. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.reals.fast.CRGroupOps CoRN.model.setoids.CRsetoid CoRN.algebra.CGroups CoRN.reals.fast.CRcorrect CoRN.tactics.CornTac