proposition: Lemma CRmult_lt_0_cancel_l : forall a b : CR, (0 < a*b)%CR -> prod (a≶0) (b≶0).
proof: Proof. pose proof (CRlt_Qlt 0 1 eq_refl). intros. destruct (CRlt_linear _ a _ H) as [H1|H1]. - split. right. apply CR_lt_ltT, H1. right. pose proof (CRinv_0_lt_compat _ (inr H1) H1). pose proof (CRmult_lt_l 0%CR (a*b)%CR _ H2) as [H3 _]. apply H3 in H0. clear H3 H2. assert (CRinvT a (inr H1) * (a * b) == b)%CR. rewrite <- CRmult_assoc. rewrite <- (CRmult_comm a), CRmult_inv_r. apply CRmult_1_l. assert (CRinvT a (inr H1) * 0 == 0)%CR by ring. apply (CRltT_wd H3 H2) in H0. apply CR_lt_ltT, H0. - destruct (CRlt_linear _ b _ H0) as [H2|H2]. + split. 2: right; apply CR_lt_ltT, H2. right. pose proof (CRmult_lt_r 0%CR a b H2) as [_ H3]. apply CR_lt_ltT, H3. assert (0 == 0 * b)%CR by ring. apply (CRltT_wd H4 (reflexivity _)), H0. + assert (a*b == (-a)*(-b))%CR by ring. apply (CRltT_wd (reflexivity 0%CR) H3) in H0. clear H3. assert (0 <= -b)%CR. { apply (CRplus_le_l _ _ b). rewrite CRplus_opp, CRplus_0_r. apply CRle_not_lt. intro abs. pose proof (CRmult_lt_r 1 a b abs)%CR as [_ H3]. apply (CRlt_irrefl a). apply (CRlt_trans _ _ _ H1), H3. assert (b == 1 * b)%CR by ring. apply (CRltT_wd H4 (reflexivity _)), H2. } pose proof (CRmult_lt_0_weaken _ _ H0 H3). split; left. apply CR_lt_ltT, (CRopp_lt_cancel a 0%CR). pose proof CRopp_0. symmetry in H5. apply (CRltT_wd H5 (reflexivity _)), H4. pose proof (@CRplus_lt_r b 0%CR (-b)%CR) as [_ H5]. apply CR_lt_ltT, H5. clear H5. assert (-b == 0-b)%CR by ring. pose proof (CRplus_opp b). symmetry in H6. apply (CRltT_wd H6 H5). clear H6 H5. pose proof (CRmult_lt_l 0 (-b) (-a) H4)%CR as [_ H5]. apply H5. clear H5. assert (0 == (-a) * 0)%CR by ring. apply (CRltT_wd H5 (reflexivity _)), 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