proposition: Lemma metric_open_ball_In X (d : X -> X -> R) : metric d -> forall x r, 0 < r <-> In (open_ball d x r) x.
proof: Proof. intros. split. - intros. constructor. rewrite metric_zero; assumption. - intros. destruct H0. rewrite metric_zero in H0; assumption. Qed.
imports: Topology(RationalsInReals SubspaceTopology) ZornsLemma(EnsemblesTactics DecidableDec) Coq(Reals ClassicalChoice Program.Subset) Coq(Lia Lra)