proposition: Lemma CRmultAssoc : associative CRmultasBinOp.
proof: Proof. intros x y z. change (x*(y*z)==(x*y)*z)%CR. rewrite <- CR_eq_as_Cauchy_IR_eq. stepl ((CRasCauchy_IR x)[*](CRasCauchy_IR (y*z)%CR)); [| now apply CR_mult_as_Cauchy_IR_mult]. stepl ((CRasCauchy_IR x)[*]((CRasCauchy_IR y)[*](CRasCauchy_IR z))); [| now apply bin_op_is_wd_un_op_rht; apply CR_mult_as_Cauchy_IR_mult]. stepr ((CRasCauchy_IR (x*y)%CR)[*](CRasCauchy_IR z)); [| now apply CR_mult_as_Cauchy_IR_mult]. stepr (((CRasCauchy_IR x)[*](CRasCauchy_IR y))[*](CRasCauchy_IR z)); [| now apply bin_op_is_wd_un_op_lft; apply CR_mult_as_Cauchy_IR_mult]. apply mult_assoc_unfolded. 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