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 m H1. exists m. intros x y. apply leEq_transitive with (nring m[*](x[-d]y)). apply H1. apply mult_resp_leEq_rht. case m. simpl in |- *. apply less_leEq. apply pos_one. intro n. astepl (Snring IR n). apply less_leEq. apply nat_less_bin_nexp. apply ax_d_nneg. apply CPsMetricSpace_is_CPsMetricSpace. Qed.
imports: CoRN.metrics.CPseudoMSpaces