proposition: Lemma scale_ball0 {R : realFieldType} (A : set R) r : (r <= 0)%R -> r *` A = set0.
proof: Proof. move=> r0; apply/seteqP; split => // x. rewrite /scale_ball; case: ifPn => // ballA. by rewrite ((ball0 _ _).2 _)// mulr_le0_ge0. 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