proposition: Lemma metric_open_ball_radius_nonpositive0 X d : @metric X d -> forall x r, open_ball d x r = Empty_set -> r <= 0.
proof: Proof. intros. apply NNPP. intros ?. apply Rnot_le_lt in H1. apply (metric_open_ball_In X d H x) in H1. rewrite H0 in H1. destruct H1. Qed.
imports: Topology(RationalsInReals SubspaceTopology) ZornsLemma(EnsemblesTactics DecidableDec) Coq(Reals ClassicalChoice Program.Subset) Coq(Lia Lra)