proposition: Lemma fasterIsRegular : is_RegularFunction (@ball X) (fun e => (approximate x (QposInf_bind f e))).
proof: Proof. intros e1 e2. simpl. apply ball_weak_le with (proj1_sig (f e1 + f e2)%Qpos). simpl. apply Qplus_le_compat. apply Hf. apply Hf. apply regFun_prf. Qed.
imports: CoRN.metric2.UniformContinuity CoRN.model.structures.QposInf CoRN.metric2.Classification CoRN.model.totalorder.QposMinMax CoRN.model.totalorder.QMinMax