proposition: Lemma sum_num_occ_alt : \sum_(a in A) N(a | t) = n.
proof: Proof. elim : n t => [[] [] // Hi|m IH y]. by rewrite (eq_bigr (fun=> 0)) // big_const iter_addn. rewrite (eq_bigr (fun a => N(a | [tuple of [:: thead y]]) + N(a | tbehead y))). by rewrite big_split /= (IH (tbehead y)) sum_num_occ_seq1 add1n. move=> a _; by apply num_occ_thead. Qed.
imports: mathcomp(all_ssreflect fingroup perm zmodp ssralg) ssr_ext f2