proposition: Lemma CRmult_lt_0_compat : forall a b : CR, (0 < a)%CR -> (0 < b)%CR -> (0 < a*b)%CR.
proof: Proof. intros a b [q H] [r H0]. exists (q*r). rewrite CRopp_0, CRplus_0_r. rewrite CRopp_0, CRplus_0_r in H. rewrite CRopp_0, CRplus_0_r in H0. pose proof (CRle_scale ('`r) b q) as [H1 _]. specialize (H1 H0). rewrite <- CRmult_scale in H1. rewrite CRmult_Qmult in H1. apply (CRle_trans H1). apply (CRplus_le_r _ _ (-scale (`q) b)%CR). rewrite CRplus_opp. rewrite <- CRmult_scale. setoid_replace (a * b - ' ` q * b)%CR with ((a-'`q)*b)%CR by (unfold equiv, msp_Equiv; ring). apply CRmult_le_0_compat. apply (CRplus_le_l _ _ ('`q)%CR). ring_simplify. exact H. apply (@CRle_trans _ ('`r)%CR). apply CRle_Qle. apply Qpos_nonneg. exact 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