proposition: Lemma metric_open_closed_ball_Included X d (x : X) r : Included (open_ball d x r) (closed_ball d x r).
proof: Proof. intros ? ?. destruct H. constructor. lra. Qed.
imports: Topology(RationalsInReals SubspaceTopology) ZornsLemma(EnsemblesTactics DecidableDec) Coq(Reals ClassicalChoice Program.Subset) Coq(Lia Lra)