proposition: Lemma CRmult_eq_0_reg_l : forall x y : CR, (~(y == 0)%CR) -> (x*y == 0)%CR -> (x == 0)%CR.
proof: Proof. intros. apply ball_stable. change (~~(x==0)%CR). intros abs. rewrite CReq_not_apart in abs. contradict abs; intro xap0. rewrite CReq_not_apart in H. contradict H; intro yap0. pose proof CRopp_0 as opp0. symmetry in opp0. destruct xap0. - pose proof (CRopp_opp x). symmetry in H. apply (CRltT_wd H opp0) in c. clear H. apply CRopp_lt_cancel in c. destruct yap0. + pose proof (CRopp_opp y). symmetry in H. apply (CRltT_wd H opp0) in c0. clear H. apply CRopp_lt_cancel in c0. pose proof (CRmult_lt_0_compat _ _ c c0) as H. revert H. apply CRle_not_lt. setoid_replace (-x*-y)%CR with (x*y)%CR by (unfold equiv, msp_Equiv; ring). rewrite H0. apply CRle_refl. + pose proof (CRmult_lt_0_compat _ _ c c0) as H. revert H. apply CRle_not_lt. rewrite opp0. setoid_replace (-x*y)%CR with (-(x*y))%CR by (unfold equiv, msp_Equiv; ring). apply CRopp_le_compat. rewrite H0. apply CRle_refl. - destruct yap0. + pose proof (CRopp_opp y). symmetry in H. apply (CRltT_wd H opp0) in c0. clear H. apply CRopp_lt_cancel in c0. pose proof (CRmult_lt_0_compat _ _ c c0) as H. revert H. apply CRle_not_lt. setoid_replace (x*-y)%CR with (-(x*y))%CR by (unfold equiv, msp_Equiv; ring). rewrite H0, <- opp0. apply CRle_refl. + pose proof (CRmult_lt_0_compat _ _ c c0) as H. revert H. apply CRle_not_lt. rewrite H0. apply CRle_refl. 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