proposition: Lemma CRmult_le_compat_l : forall (x y z: CR), (0 <= z -> x <= y -> z*x <= z*y)%CR.
proof: Proof. intros. pose proof (@CRplus_le_r x y (-x)%CR) as [H1 _]. specialize (H1 H0). rewrite CRplus_opp in H1. apply (CRmult_le_0_compat _ _ H) in H1. pose proof (@CRplus_le_l 0%CR (z*(y-x))%CR (x*z)%CR) as [H2 _]. specialize (H2 H1). ring_simplify in H2. rewrite CRmult_comm in H2. exact H2. 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