proposition: Lemma num_occ_flatten (A : finType) (a : A) ss : N(a|flatten ss) = (\sum_(s <- ss) N(a|s))%nat.
proof: Proof. rewrite /num_occ. elim: ss => [|s ss IH] /=; first by rewrite big_nil. by rewrite big_cons /= count_cat IH. Qed.
imports: mathcomp(all_ssreflect fingroup perm zmodp ssralg) ssr_ext f2