proposition: Lemma lip_c_imp_lip : forall (A B : CPsMetricSpace) (f : CSetoid_fun A B) (C : IR), lipschitz_c f C -> lipschitz' f.
proof: Proof. unfold lipschitz_c. unfold lipschitz'. intros. assert ({n : nat| C [<=] nring n}). apply Archimedes. destruct X as [n H1]. exists n. intros. assert (f x[-d]f y [<=] C[*](x[-d]y)). apply H. apply leEq_transitive with (C[*](x[-d]y)); auto. apply mult_resp_leEq_rht; auto. apply ax_d_nneg. apply CPsMetricSpace_is_CPsMetricSpace. Qed.
imports: CoRN.metrics.CPseudoMSpaces