proposition: Lemma isopsmetry_imp_lipschitz : forall (X Y : CPsMetricSpace) (f : CSetoid_fun X Y), isopsmetry f -> lipschitz' f.
proof: Proof. intros X Y f. unfold isopsmetry in |- *. unfold equivalent_psmetric in |- *. intro H. elim H. clear H. intros H0 H1. elim H1. clear H1. intros H10 H11. elim H11. clear H11. intros H110 H111. unfold lipschitz' in |- *. elim H111. clear H111. simpl in |- *. intros n H111'. exists (S n). simpl in |- *. exact H111'. Qed.
imports: CoRN.metrics.IR_CPMSpace