proposition: Lemma CRAbsSmall_ball : forall (x y:CR) (e:Q), (-'e <= x-y /\ x-y <= 'e)%CR <-> ball e x y.
proof: Proof. intros x y e. split. - intros [H1 H2]. rewrite <- (doubleSpeed_Eq x). rewrite <- (doubleSpeed_Eq (doubleSpeed x)). rewrite <- (doubleSpeed_Eq y). rewrite <- (doubleSpeed_Eq (doubleSpeed y)). apply regFunBall_e. intros d. assert (H1':=H1 d). assert (H2':=H2 d). clear H1 H2. simpl. set (x':=approximate x ((1#2)*((1#2)*d))%Qpos). set (y':=approximate y ((1#2)*((1#2)*d))%Qpos). change (-proj1_sig d <= x' - y' + - - e)%Q in H1'. change (-proj1_sig d <= e + - (x' - y'))%Q in H2'. rewrite -> Qle_minus_iff in *. apply ball_weak. apply Qpos_nonneg. split; simpl; rewrite -> Qle_minus_iff. rewrite Qopp_involutive. do 2 rewrite Qopp_involutive in H1'. rewrite (Qplus_comm (proj1_sig d)). rewrite Qplus_assoc. exact H1'. rewrite <- Qplus_assoc, Qplus_comm. rewrite Qopp_involutive in H2'. exact H2'. - intros H. rewrite <- (doubleSpeed_Eq x) in H. rewrite <- (doubleSpeed_Eq y) in H. split; intros d; destruct (H ((1#2)*d)%Qpos ((1#2)*d)%Qpos) as [H1 H2]; clear H; set (x':=(approximate (doubleSpeed x) ((1 # 2) * d)%Qpos)) in *; set (y':=(approximate (doubleSpeed y) ((1 # 2) * d)%Qpos)) in *. autorewrite with QposElim in H1. change (- ((1 # 2) * proj1_sig d + e + (1 # 2) * proj1_sig d)<=x' - y')%Q in H1. change (-proj1_sig d <= x' - y' + - - e)%Q. rewrite -> Qle_minus_iff. rewrite -> Qle_minus_iff in H1. setoid_replace (x' - y' + - - e + - - ` d)%Q with (x' - y' + - - ((1 # 2) * proj1_sig d + e + (1 # 2) * proj1_sig d))%Q by (unfold equiv, stdlib_rationals.Q_eq; ring). assumption. autorewrite with QposElim in H2. change (x' - y'<=((1 # 2) * proj1_sig d + e + (1 # 2) * proj1_sig d))%Q in H2. change (-proj1_sig d <= e + - (x' - y'))%Q. rewrite -> Qle_minus_iff. rewrite -> Qle_minus_iff in H2. setoid_replace (e + - (x' - y') + - - ` d)%Q with ((1 # 2) * proj1_sig d + e + (1 # 2) * proj1_sig d + - (x' - y'))%Q by (unfold equiv, stdlib_rationals.Q_eq; ring). assumption. 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