proposition: Lemma metric_nonneg : metric -> forall x y : X, d x y >= 0.
proof: Proof. intros. pose proof (triangle_inequality H x y x). rewrite (metric_sym H y x) in H0. rewrite (metric_zero H) in H0. lra. Qed.
imports: Topology(RationalsInReals SubspaceTopology) ZornsLemma(EnsemblesTactics DecidableDec) Coq(Reals ClassicalChoice Program.Subset) Coq(Lia Lra)