proposition: Lemma CRmult_lt_r : forall (x y z: CR), (0 < z)%CR -> prod (x < y -> x*z < y*z)%CR (x*z < y*z -> x < y)%CR.
proof: Proof. assert (forall (x y z: CR), (0 < z)%CR -> (x < y -> x*z < y*z)%CR). { intros. pose proof (@CRplus_lt_r x y (-x)%CR) as [H1 _]. apply H1 in H0. clear H1. apply (CRltT_wd (CRplus_opp x) (reflexivity (y-x)%CR)) in H0. apply (CRmult_lt_0_compat _ _ H) in H0. pose proof (@CRplus_lt_r 0%CR (z*(y-x))%CR (x*z)%CR) as [H1 _]. apply H1 in H0. clear H1. assert (z*(y-x)+x*z == y*z)%CR by ring. pose proof (CRltT_wd (CRplus_0_l (x*z)%CR) H1). apply H2 in H0. exact H0. } split. apply X, H. intros. pose proof (CRinv_0_lt_compat _ (inr H) H). specialize (X (x*z)%CR (y*z)%CR _ H1 H0). assert (x * z * CRinvT z (inr H) == x)%CR. { rewrite CRmult_assoc, CRmult_inv_r. apply CRmult_1_r. } assert (y * z * CRinvT z (inr H) == y)%CR. { rewrite CRmult_assoc, CRmult_inv_r. apply CRmult_1_r. } apply (CRltT_wd H2 H3) in X. exact X. 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