proposition: Lemma uc_ex_prf (u: UniformlyContinuousFunction) (e: QposInf) (a b: X): ball_ex (mu_ex u e) a b -> ball_ex e (ucFun u a) (ucFun u b).
proof: Proof. Proof with auto. intros. destruct e... simpl in *. apply uc_prf. assumption. Qed.
imports: CoRN.model.totalorder.QposMinMax CoRN.metric2.Metric CoRN.model.structures.QposInf CoRN.stdlib_omissions.List