proposition: Lemma isopsmetry_imp_bij : forall (X Y : CPsMetricSpace) (f : CSetoid_fun X Y), isopsmetry f -> bijective f.
proof: Proof. intros X Y f H. unfold isopsmetry in H. elim H. intuition. Qed.
imports: CoRN.metrics.IR_CPMSpace