fact: Definition prop_near1 {X} {fX : filteredType X} (x : fX) P (phP : ph {all1 P}) := nbhs x P.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed