proposition: Lemma sum_num_occ_all : \sum_(i < #|A|) N(enum_val i | t) = n.
proof: Proof. symmetry. rewrite -{1}sum_num_occ_alt. rewrite (reindex_onto enum_rank enum_val) /= => [|i _]; last by rewrite enum_valK. apply eq_big => x0 ; by rewrite enum_rankK // eqxx. Qed.
imports: mathcomp(all_ssreflect fingroup perm zmodp ssralg) ssr_ext f2