fact: Record metric : Prop := { metric_sym: forall x y:X, d x y = d y x; triangle_inequality: forall x y z:X, d x z <= d x y + d y z; metric_zero: forall x:X, d x x = 0; metric_strict: forall x y:X, d x y = 0 -> x = y }.
imports: Topology(RationalsInReals SubspaceTopology) ZornsLemma(EnsemblesTactics DecidableDec) Coq(Reals ClassicalChoice Program.Subset) Coq(Lia Lra)