proposition: Lemma CRmult_lt_l (x y z: CR): (0 < z)%CR -> prod (x < y -> z*x < z*y)%CR (z*x < z*y -> x < y)%CR.
proof: Proof. split. - intros. apply (CRltT_wd (CRmult_comm x z) (CRmult_comm y z)). pose proof (CRmult_lt_r x y z H) as [H1 _]. apply H1, H0. - intros. pose proof (CRmult_lt_r x y z H) as [_ H1]. apply H1. clear H1. apply (CRltT_wd (CRmult_comm z x) (CRmult_comm z y)). apply H0. 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