proposition: Lemma nbhs_ex (x : T) (P : T -> Prop) : nbhs x P -> {d : {posnum R} | forall y, ball x d%:num y -> P y}.
proof: Proof. move=> /nbhs_ballP xP. pose D := [set d : R^o | d > 0 /\ forall y, ball x d y -> P y]. have [|d_gt0 dP] := @getPex _ D; last by exists (PosNum d_gt0). by move: xP => [e bP]; exists (e : R). 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