proposition: Lemma filter_imply [T : Type] [P : Prop] [f : set T] [F : set_system T] : Filter F -> (P -> \near F, f F) -> \near F, P -> f F.
proof: Proof. move=> ? PF; near do move=> /asboolP. by case: asboolP=> [/PF|_]; by [apply: filterS|apply: nearW]. Unshelve. all: by end_near. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed