proposition: Lemma nbhs_singleton (p : M) A : nbhs p A -> A p.
proof: Proof. rewrite nbhsE nbhs_E => - [B entB sBpA]. by apply: sBpA; apply: entourage_refl entB _ _. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed