proposition: Lemma CRAbsSmall_ball : forall (x y:CR) (e:Q), AbsSmall (R:=CRasCOrdField) (inject_Q_CR e) ((x:CRasCOrdField)[-]y) <-> 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) in H1'. change (-proj1_sig d <= e + - (x' - y')) 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') in H1. change (-proj1_sig d <= x' - y' + - - e). rewrite -> Qle_minus_iff. rewrite -> Qle_minus_iff in H1. replace RHS with (x' - y' + - - ((1 # 2) * proj1_sig d + e + (1 # 2) * proj1_sig d)) by ring. assumption. autorewrite with QposElim in H2. change (x' - y'<=((1 # 2) * proj1_sig d + e + (1 # 2) * proj1_sig d)) in H2. change (-proj1_sig d <= e + - (x' - y')). rewrite -> Qle_minus_iff. rewrite -> Qle_minus_iff in H2. replace RHS with ((1 # 2) * proj1_sig d + e + (1 # 2) * proj1_sig d + - (x' - y')) by ring. assumption. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QposMinMax CoRN.reals.fast.CRFieldOps CoRN.model.ordfields.CRordfield CoRN.reals.CReals CoRN.reals.fast.CRcorrect CoRN.model.metric2.Qmetric CoRN.tactics.CornTac