proposition: Lemma uni_continuous'_imp_uni_continuous'' : forall (A B : CPsMetricSpace) (f : CSetoid_fun A B), uni_continuous' f -> uni_continuous'' f.
proof: Proof. intros A B f. unfold uni_continuous' in |- *. unfold uni_continuous'' in |- *. apply choice with (P := fun n m : nat => forall x y : A, x[-d]y[<=]one_div_succ m -> f x[-d]f y[<=]one_div_succ n). Qed.
imports: CoRN.metrics.CPseudoMSpaces