proposition: Lemma powerset_filter_fromP C : F C -> powerset_filter_from [set W | F W /\ W `<=` C].
proof: Proof. move=> FC; exists [set W | F W /\ W `<=` C] => //; split; first by move=> ? []. by move=> A B [_ AC] FB /subset_trans/(_ AC). by exists C; split. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed