proposition: Lemma CRmult_lt_0_weaken : forall (x y : CR), (0 < x * y -> 0 <= y -> 0 < x)%CR.
proof: Proof. intros. pose proof (CRlt_Qlt 0 1 eq_refl) as zeroLtOne. destruct (CRlt_linear 0%CR x 1%CR zeroLtOne) as [H3|H3]. - exact H3. - clear zeroLtOne. apply CRlt_le_weak in H3. pose proof (CRmult_le_compat_l x 1%CR y H0 H3) as H1. rewrite CRmult_1_r in H1. rewrite CRmult_comm in H1. apply (@CRlt_le_trans 0%CR (x*y) y H) in H1. assert (0 == 0*y)%CR by ring. apply (CRltT_wd H2 (reflexivity _)) in H. clear H2. apply (CRmult_lt_r 0%CR x y). exact H1. exact H. 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