proposition: Lemma is_uc_uc_compose : forall X Y Z, is_UniformlyContinuousFunction (@uc_compose_uc0 X Y Z) Qpos2QposInf.
proof: Proof. intros X Y Z e x y Hxy. split. apply Qpos_nonneg. intro z. split. apply Qpos_nonneg. intro z0. simpl. apply Hxy. Qed.
imports: CoRN.model.totalorder.QposMinMax CoRN.metric2.Metric CoRN.model.structures.QposInf CoRN.stdlib_omissions.List