proposition: Lemma num_occ_thead (ta : n.+1.-tuple A) : N(a | ta) = N(a | [tuple of [:: thead ta]]) + N(a | tbehead ta).
proof: Proof. by rewrite {1}(tuple_eta ta) /num_occ /= addn0. Qed.
imports: mathcomp(all_ssreflect fingroup perm zmodp ssralg) ssr_ext f2