proposition: Lemma filter_near_of T F (P : @in_filter T F) (Q : set T) : Filter F -> (forall x, prop_of P x -> Q x) -> F Q.
proof: Proof. by move: P => [P FP] FF /=; rewrite prop_ofE /= => /filterS; apply. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed