proposition: Lemma regFun_prf_ex : forall (r : Complete) (e1 e2 : QposInf), ball_ex (e1 + e2) (approximate r e1) (approximate r e2).
proof: Proof. intros r [e1|] [e2|]; try constructor. apply (@regFun_prf X (@ball X)). Qed.
imports: CoRN.metric2.UniformContinuity CoRN.model.structures.QposInf CoRN.metric2.Classification CoRN.model.totalorder.QposMinMax CoRN.model.totalorder.QMinMax