proposition: Lemma pair_uc_l : forall y:Y, @is_UniformlyContinuousFunction X XY (fun x => (x,y)) Qpos2QposInf.
proof: Proof. intros y e a b H. split; auto. apply ball_refl. apply QposMinMax.Qpos_nonneg. Qed.
imports: CoRN.metric2.ProductMetric CoRN.metric2.Complete