proposition: Lemma count_enum_cards (T : finType) (A : {set T}) (P : {pred T}) : count P (enum A) = #|[set x in A | P x]|.
proof: Proof. rewrite -size_filter cardsE cardE. apply/perm_size/uniq_perm; rewrite ?filter_uniq -?enumT ?enum_uniq //. by move=> x; rewrite !(mem_enum,mem_filter,unfold_in) andbC. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph sgraph) GraphTheory(dom partition coloring) mathcomp(ssrint) mathcomp(all_algebra)