proposition: Lemma CRmult_le_0_reg_l : forall a b : CR, ~((0 < a)%CR -> False) -> (0 <= a * b)%CR -> (0 <= b)%CR.
proof: Proof. intros. apply CRle_not_lt. intro abs. contradict H; intro H. rewrite <- CRopp_0 in H0. setoid_replace (a*b)%CR with (-(a*-b))%CR in H0 by (unfold equiv, msp_Equiv; ring). apply CRopp_le_cancel in H0. pose proof (CRle_not_lt (a*-b)%CR 0%CR) as [H1 _]. specialize (H1 H0). contradict H1. clear H0. apply CRmult_lt_0_compat. exact H. apply (CRltT_wd CRopp_0 (reflexivity _)). apply CRopp_lt_compat, abs. 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