proposition: Lemma CRabs_nlt : forall x y : CR, (((y < x)%CR -> False) /\ ((y < -x)%CR -> False)) <-> ((y < CRabs x)%CR -> False).
proof: Proof. split. - intros [H H0] H1. apply CRle_not_lt in H1. contradiction. clear H2 H1. pose proof (CRdistance_CRle y x 0%CR) as [H2 _]. unfold CRdistance in H2. rewrite CRopp_0, CRplus_0_r in H2. apply H2. clear H2. split. apply (CRplus_le_r _ _ y). apply CRle_not_lt in H. ring_simplify. exact H. apply CRle_not_lt in H0. rewrite (CRplus_le_r _ _ x) in H0. ring_simplify in H0. exact H0. - split. apply CRle_not_lt in H. apply CRle_not_lt. apply (@CRle_trans _ (CRabs x)). 2: exact H. apply CRle_abs. apply CRle_not_lt in H. apply CRle_not_lt. apply (@CRle_trans _ (CRabs x)). 2: exact H. rewrite <- CRabs_opp. apply CRle_abs. Qed.
imports: Coq.Reals.Abstract.ConstructiveReals CoRN.model.metric2.Qmetric CoRN.model.metric2.CRmetric CoRN.reals.fast.CRFieldOps CoRN.reals.fast.CRArith CoRN.reals.fast.CRabs CoRN.model.totalorder.QposMinMax Coq.Logic.ConstructiveEpsilon