proposition: Lemma is_scale_ball (A : set R) (k : R) : is_ball A -> is_ball (k *` A).
proof: Proof. move=> Aball. have [k0|k0] := leP 0 k. by rewrite (ballE Aball) (scale_ballE _ _ k0); exact: is_ball_ball. rewrite (_ : _ *` _ = set0); first exact: is_ball0. apply/seteqP; split => // x. by rewrite /scale_ball Aball (ball0 _ _).2// nmulr_rle0. 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