proposition: Lemma ereal_nbhs_singleton (p : \bar R) (A : set (\bar R)) : ereal_nbhs p A -> A p.
proof: Proof. move: p => -[p | [M [Mreal MA]] | [M [Mreal MA]]] /=; [|exact: MA | exact: MA]. move=> /nbhs_ballP[_/posnumP[e]]; apply; exact/ballxx. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(fsbigop cardinality set_interval) reals signed topology constructive_ereal