proposition: Lemma lipschitz_imp_lipschitz' : forall (A B : CPsMetricSpace) (f : CSetoid_fun A B), lipschitz f -> lipschitz' f.
proof: Proof. intros A B f. unfold lipschitz in |- *. intro H. unfold lipschitz' in |- *. elim H. intros n H0. elim Archimedes with ((Two:IR)[^]n). intros m H1. exists m. intros x y. apply leEq_transitive with ((Two:IR)[^]n[*](x[-d]y)). apply H0. apply mult_resp_leEq_rht. exact H1. apply ax_d_nneg. apply CPsMetricSpace_is_CPsMetricSpace. Qed.
imports: CoRN.metrics.CPseudoMSpaces