proposition: Lemma Cunit_fun_prf (x:X) : is_RegularFunction (@ball X) (fun _ => x).
proof: Proof. intros d1 d2. apply ball_refl. apply (Qpos_nonneg (d1+d2)). Qed.
imports: CoRN.metric2.UniformContinuity CoRN.model.structures.QposInf CoRN.metric2.Classification CoRN.model.totalorder.QposMinMax CoRN.model.totalorder.QMinMax