proposition: Lemma ex_ball_sig (x : T) (P : set T) : ~ (forall eps : {posnum R}, ~ (ball x eps%:num `<=` ~` P)) -> {d : {posnum R} | ball x d%:num `<=` ~` P}.
proof: Proof. rewrite forallNE notK => exNP. pose D := [set d : R^o | d > 0 /\ ball x d `<=` ~` P]. have [|d_gt0] := @getPex _ D; last by exists (PosNum d_gt0). by move: exNP => [e eP]; exists e%:num. 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