proposition: Lemma ball0 (a r : R) : ball a r = set0 <-> r <= 0.
proof: Proof. split. move=> /seteqP[+ _] => H; rewrite leNgt; apply/negP => r0. by have /(_ (ballxx _ r0)) := H a. move=> r0; apply/seteqP; split => // y; rewrite /ball/=. by move/lt_le_trans => /(_ _ r0); rewrite normr_lt0. 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