proposition: Lemma nbhs_filter (p : M) : ProperFilter (nbhs p).
proof: Proof. rewrite nbhsE nbhs_E; apply filter_from_proper; last first. by move=> A entA; exists p; apply: entourage_refl entA _ _. apply: filter_from_filter. by exists setT; apply: @filterT entourage_filter. move=> A B entA entB; exists (A `&` B) => //. exact: (@filterI _ _ entourage_filter). Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed