proposition: Lemma CRmult_lt_cancel_l : forall a b c : CR, (a*b < a*c)%CR -> (prod (a≶0) (b≶c)).
proof: Proof. intros. pose proof (CRplus_lt_l (a*b) (a*c) (-a*b))%CR as [H0 _]. specialize (H0 H). assert (- a * b + a * b == 0)%CR by ring. assert (- a * b + a * c == a*(c-b))%CR by ring. apply (CRltT_wd H1 H2) in H0. clear H1 H2. apply CRmult_lt_0_cancel_l in H0. destruct H0. split. exact a0. destruct a1. - right. apply CR_lt_ltT in H0. pose proof (CRplus_lt_l (c-b) (0) b)%CR as [H1 _]. specialize (H1 H0). assert (b + (c - b) == c)%CR by ring. assert (b + 0 == b)%CR by ring. apply (CRltT_wd H2 H3) in H1. apply CR_lt_ltT, H1. - left. apply CR_lt_ltT in H0. pose proof (CRplus_lt_l 0 (c-b) b)%CR as [H1 _]. specialize (H1 H0). assert (b + (c - b) == c)%CR by ring. assert (b + 0 == b)%CR by ring. apply (CRltT_wd H3 H2) in H1. apply CR_lt_ltT, H1. 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