proposition: Lemma Cunit_prf : is_UniformlyContinuousFunction Cunit_fun Qpos2QposInf.
proof: Proof. intros e a b Hab d1 d2. simpl in *. assert (QposEq (d1+e+d2) (e+(d1+d2))). { unfold QposEq; simpl; ring. } unfold QposEq in H. rewrite H. clear H. apply ball_weak. apply Qpos_nonneg. assumption. Qed.
imports: CoRN.metric2.UniformContinuity CoRN.model.structures.QposInf CoRN.metric2.Classification CoRN.model.totalorder.QposMinMax CoRN.model.totalorder.QMinMax