proposition: Lemma regFunBall_e : forall (x y:Complete) (e:Q), (forall d:Qpos, ball (proj1_sig d + e + proj1_sig d) (approximate x d) (approximate y d)) -> ball e x y.
proof: Proof. intros x y e H. apply ball_closed. intros d dpos. setoid_replace (e + d) with ((1#4)*d + ((1#4)*d+ e+(1#4)*d) + (1#4)*d) by (simpl; ring). apply (regFunBall_ball x y ((1 # 4) * d + e + (1 # 4) * d)%Q ((1#4)*exist _ _ dpos)%Qpos ((1#4)*exist _ _ dpos)%Qpos ). apply (H ((1#4)*(exist _ _ dpos))%Qpos). Qed.
imports: CoRN.metric2.UniformContinuity CoRN.model.structures.QposInf CoRN.metric2.Classification CoRN.model.totalorder.QposMinMax CoRN.model.totalorder.QMinMax