proposition: Lemma count_set_of_card (p : pred nat) P : count p [seq #{x} | x in P] = #|P :&: [set x | p #{x}]|.
proof: Proof. Proof using. rewrite cardE -size_filter /enum_mem -enumT /=. rewrite filter_map size_map; congr size. rewrite -filter_predI -enumT /=; apply eq_filter. by move=> S; rewrite !inE andbC. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype