proposition: Lemma is_RegularFunction_wd : forall (X : MetricSpace) (x y:QposInf -> X), (forall q : Qpos, msp_eq (x q) (y q)) -> is_RegularFunction (@ball X) x -> is_RegularFunction (@ball X) y.
proof: Proof. intros. intros e1 e2. rewrite <- H, <- H. apply H0. Qed.
imports: CoRN.metric2.UniformContinuity CoRN.model.structures.QposInf CoRN.metric2.Classification CoRN.model.totalorder.QposMinMax CoRN.model.totalorder.QMinMax