proposition: Lemma have_near (U : Type) (fT : filteredType U) (x : fT) (P : Prop) : ProperFilter (nbhs x) -> (\forall x \near x, P) -> P.
proof: Proof. by move=> FF nP; have [] := @filter_ex _ _ FF (fun=> P). Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed