proposition: Lemma uc_prf_smaller : forall (f:UniformlyContinuousFunction) (mu2 : Qpos -> QposInf), (forall e, QposInf_le (mu2 e) (mu f e)) -> is_UniformlyContinuousFunction (ucFun f) mu2.
proof: Proof. intros f my2 H. eapply is_UniformlyContinuousFunction_wd. intros; reflexivity. apply H. apply uc_prf. Qed.
imports: CoRN.model.totalorder.QposMinMax CoRN.metric2.Metric CoRN.model.structures.QposInf CoRN.stdlib_omissions.List