proposition: Lemma near_skip_subproof T F (P Q : @in_filter T F) (G : set T) (FF : Filter F) : locked_with near_key (forall x, prop_of P x -> G x) -> locked_with near_key (forall x, prop_of (in_filterI FF P Q) x -> G x).
proof: Proof. rewrite !unlock => FG x /=; rewrite !prop_ofE /= => -[Px Qx]. by have /= := FG x; apply; rewrite prop_ofE. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed