proposition: Lemma isometry_injective {X Y : Type} d0 d1 (f : X -> Y) : metric d0 -> metric d1 -> isometry d0 d1 f -> injective f.
proof: Proof. intros Hd0 Hd1 Hf x0 x1 Hx. eapply metric_strict; eauto. rewrite <- Hf, Hx. apply metric_zero; auto. Qed.
imports: Topology(RationalsInReals SubspaceTopology) ZornsLemma(EnsemblesTactics DecidableDec) Coq(Reals ClassicalChoice Program.Subset) Coq(Lia Lra)