proposition: Lemma CRle_not_lt (x y: CR): (x <= y)%CR <-> (y < x -> False)%CR.
proof: Proof. split. - intros H [q H0]. apply (CRplus_le_compat _ _ _ _ H) in H0. setoid_replace (y + (x-y))%CR with (x+0) in H0 by (unfold equiv, msp_Equiv; ring). apply CRplus_le_l in H0. apply CRle_Qle in H0. apply (Qle_not_lt _ _ H0 (Qpos_ispos q)). - intros. assert (forall z:CR, (0 < z -> False) -> z <= 0) as zero_irrefl. { clear H x y. intros z H0. unfold CRltT in H0. unfold CRle. apply (@CRnonNeg_wd (-z)). ring. intro q. apply Qnot_lt_le. intro abs. apply H0. clear H0. apply (@CRpos_wd z). ring. simpl in abs. apply Qlt_minus_iff in abs. rewrite Qopp_involutive, Qplus_comm in abs. exists (exist (Qlt 0) _ abs). intro r. simpl. unfold Cap_raw; simpl. pose proof (regFun_prf z q ((1#2)*r)%Qpos). apply AbsSmall_Qabs in H. apply (Qle_trans _ _ _ (Qle_Qabs _)) in H. apply (Qplus_le_l _ _ (approximate z q + `r)). simpl. ring_simplify. apply (Qplus_le_l _ _ (approximate z ((1#2)*r)%Qpos)) in H. ring_simplify in H. rewrite (Qplus_comm (`r)). apply (Qle_trans _ _ _ H). rewrite <- Qplus_assoc, <- Qplus_assoc. apply Qplus_le_r. rewrite Qplus_comm. apply Qplus_le_l. simpl. rewrite <- (Qmult_1_l (`r)) at 2. apply Qmult_le_r. apply Qpos_ispos. discriminate. } assert (0<x-y -> False)%CR. { intros [q H0]. apply H. clear H zero_irrefl. exists q. unfold CRle. unfold CRle in H0. setoid_replace (x - y - ' 0%Q - ' ` q)%CR with (x - y - ' ` q) in H0 by (unfold equiv, msp_Equiv; ring). exact H0. } apply (CRplus_le_r _ _ (-y)). rewrite CRplus_opp. apply zero_irrefl, 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