proposition: Lemma CRmult_strext : bin_op_strext CRasCSetoid CRmult.
proof: Proof. intros x1 x2 y1 y2 H. simpl in *. autorewrite with CRtoCauchy_IR in H. assert (X:(CRasCauchy_IR x1[*]CRasCauchy_IR y1)[#](CRasCauchy_IR x2[*]CRasCauchy_IR y2)). stepl (CRasCauchy_IR (x1*y1)%CR); [| now apply eq_symmetric; apply CR_mult_as_Cauchy_IR_mult]. stepr (CRasCauchy_IR (x2*y2)%CR); [| now apply eq_symmetric; apply CR_mult_as_Cauchy_IR_mult]. 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.CRFieldOps CoRN.model.abgroups.CRabgroup CoRN.algebra.CRings CoRN.reals.fast.CRcorrect CoRN.tactics.Rational CoRN.tactics.CornTac