proposition: Lemma regFunBall_e2 : forall (X: MetricSpace) (x y:Complete X) (e:Q), (forall d:Qpos, ball (proj1_sig d + e) (approximate x ((1#2)*d)%Qpos) (approximate y ((1#2)*d)%Qpos)) -> ball e x y.
proof: Proof. intros X x y e H. apply ball_closed. intros d dpos. setoid_replace (e + d)%Q with ((1#2)*((1#2)*d) + ((1#2)*((1#2)*d) + e+(1#2)*((1#2)*d)) + (1#2)*((1#2)*d))%Q by (unfold canonical_names.equiv, stdlib_rationals.Q_eq; simpl; ring). apply (regFunBall_ball x y ((1 # 2) * ((1#2)*d) + e + (1 # 2) * ((1#2)*d))%Q ((1#2)*((1#2)*exist _ _ dpos))%Qpos ((1#2)*((1#2)*exist _ _ dpos))%Qpos ). setoid_replace ((1 # 2) * ((1 # 2) * d) + e + (1 # 2) * ((1 # 2) * d))%Q with ((1 # 2) * d + e)%Q by (unfold canonical_names.equiv, stdlib_rationals.Q_eq; simpl; ring). apply (H ((1#2)*(exist _ _ dpos))%Qpos). Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QposMinMax CoRN.reals.fast.CRArith CoRN.model.metric2.Qmetric Coq.QArith.Qabs CoRN.model.totalorder.QMinMax CoRN.logic.Stability