proposition: Lemma closed_ball_radius_negative X d : @metric X d -> forall x r, r < 0 <-> closed_ball d x r = Empty_set.
proof: Proof. intros. split. - intros. apply Extensionality_Ensembles; split; red; intros; try contradiction. destruct H1. pose proof (metric_nonneg X d H x x0). lra. - intros. apply NNPP. intros ?. apply not_Rlt in H1. apply Rge_le in H1. apply (metric_closed_ball_In X d H x r) in H1. rewrite H0 in H1. destruct H1. Qed.
imports: Topology(RationalsInReals SubspaceTopology) ZornsLemma(EnsemblesTactics DecidableDec) Coq(Reals ClassicalChoice Program.Subset) Coq(Lia Lra)