proposition: Lemma filter_const {T : Type} {F} {FF: @ProperFilter T F} (P : Prop) : F (fun=> P) -> P.
proof: Proof. by move=> FP; case: (filter_ex FP). Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed