proposition: Lemma filter_from_proper {I T : Type} (D : set I) (B : I -> set T) : Filter (filter_from D B) -> (forall i, D i -> B i !=set0) -> ProperFilter (filter_from D B).
proof: Proof. move=> FF BN0; apply: Build_ProperFilter=> P [i Di BiP]. by have [x Bix] := BN0 _ Di; exists x; apply: BiP. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed