proposition: Lemma subset_filter_proper {T F} {FF : Filter F} (D : set T) : (forall P, F P -> ~ ~ exists x, D x /\ P x) -> ProperFilter (subset_filter F D).
proof: Proof. move=> DAP; apply: Build_ProperFilter'; rewrite /subset_filter => subFD. by have /(_ subFD) := DAP (~` D); apply => -[x [dx /(_ dx)]]. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed