proposition: Lemma uc_id_prf (X:MetricSpace) : is_UniformlyContinuousFunction (fun (x:X) => x) Qpos2QposInf.
proof: Proof. intros e a b Hab. assumption. Qed.
imports: CoRN.model.totalorder.QposMinMax CoRN.metric2.Metric CoRN.model.structures.QposInf CoRN.stdlib_omissions.List