proposition: Lemma closed_ball0 (R : realFieldType) (a r : R) : r <= 0 -> closed_ball a r = set0.
proof: Proof. move=> /ball0 r0; apply/seteqP; split => // y. by rewrite /closed_ball r0 closure0. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrint ssrnum finmap matrix) mathcomp(rat interval zmodp vector fieldext falgebra) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality set_interval Rstruct) ereal reals signed topology prodnormedzmodule