proposition: Lemma ballE (A : set R) : is_ball A -> A = ball (cpoint A) (radius A)%:num.
proof: Proof. move=> ballA; apply/seteqP; split => [x /is_ballP|x Ax]; first exact. by move: ballA => /eqP ->. 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