proposition: Lemma count_map_muln (x : A) : count c [seq f x i | i <- em] = (a x * count b em)%nat.
proof: Proof. elim: em => [/=|y ? IH]; first by rewrite muln0. by rewrite /= -(eqP (abc x y)) IH mulnDr mulnb. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist