proposition: Lemma CRmult_comm_bounded (x y: CR) (b:Qpos) : (' (- ` b)%Q <= x)%CR -> (x <= 'proj1_sig b)%CR -> (' (- ` b)%Q <= y)%CR -> (y <= 'proj1_sig b)%CR -> CRmult_bounded b x y == CRmult_bounded b y x.
proof: Proof. intros. rewrite CRmult_uncurry_eq, CRmult_uncurry_eq; try assumption. apply Cmap2_comm. intros. apply Qball_0, Qmult_comm. Qed.
imports: CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QMinMax CoRN.model.totalorder.QposMinMax Coq.setoid_ring.Ring_theory Coq.Setoids.Setoid Coq.QArith.QArith Coq.QArith.Qabs Coq.QArith.Qround CoRN.metric2.Complete CoRN.metric2.ProductMetric CoRN.reals.fast.CRFieldOps CoRN.model.metric2.Qmetric CoRN.logic.Stability Coq.Logic.ConstructiveEpsilon CoRN.util.Qdlog MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders