proposition: Lemma regFunBall_wd : forall (e1 e2:Q) (x y : RegularFunction (@ball X)), (e1 == e2) -> (regFunBall e1 x y <-> regFunBall e2 x y).
proof: Proof. unfold regFunBall. split. - intros. rewrite <- H. apply H0. - intros. rewrite H. apply H0. Qed.
imports: CoRN.metric2.UniformContinuity CoRN.model.structures.QposInf CoRN.metric2.Classification CoRN.model.totalorder.QposMinMax CoRN.model.totalorder.QMinMax