proposition: Lemma d_restriction_metric: metric d_restriction.
proof: Proof. constructor; intros; try destruct x; try destruct y; try destruct z; try apply subset_eq_compat; apply d_metric; trivial. Qed.
imports: Topology(RationalsInReals SubspaceTopology) ZornsLemma(EnsemblesTactics DecidableDec) Coq(Reals ClassicalChoice Program.Subset) Coq(Lia Lra)