proposition: Lemma ball_approx_l : forall (x:Complete) (e:Qpos), ball (proj1_sig e) (Cunit (approximate x e)) x.
proof: Proof. pose ball_approx_r. pose ball_sym. auto. Qed.
imports: CoRN.metric2.UniformContinuity CoRN.model.structures.QposInf CoRN.metric2.Classification CoRN.model.totalorder.QposMinMax CoRN.model.totalorder.QMinMax