proposition: Lemma ball_approx_r : forall (x:Complete) (e:Qpos), ball (proj1_sig e) x (Cunit (approximate x e)).
proof: Proof. intros x e d1 d2. simpl. apply ball_weak. apply Qpos_nonneg. apply regFun_prf. Qed.
imports: CoRN.metric2.UniformContinuity CoRN.model.structures.QposInf CoRN.metric2.Classification CoRN.model.totalorder.QposMinMax CoRN.model.totalorder.QMinMax