proposition: Lemma is_uc_uc_compose0 : forall X Y Z (f:Y-->Z), is_UniformlyContinuousFunction (@uc_compose X Y Z f) (mu f).
proof: Proof. intros X Y Z f e x y Hxy. split. apply Qpos_nonneg. intro z. simpl. simpl in Hxy. apply uc_prf. destruct (mu f e); auto. apply Hxy. Qed.
imports: CoRN.model.totalorder.QposMinMax CoRN.metric2.Metric CoRN.model.structures.QposInf CoRN.stdlib_omissions.List