proposition: Lemma is_ball_closureP (A : set R) x : is_ball A -> closure A x -> `|cpoint A - x| <= (radius A)%:num.
proof: Proof. move=> ballP cAx. have : closed_ball (cpoint A) (radius A)%:num x by rewrite /closed_ball -ballE. by have [r0|r0] := ltP 0 (radius A)%:num; [rewrite closed_ballE| rewrite closed_ball0]. 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