proposition: Lemma sum_num_occ_rec (k : 'I_#|A|) : sum_num_occ k.+1 = sum_num_occ k + N(enum_val k | ta).
proof: Proof. rewrite /sum_num_occ (bigD1 k) /=; last by exact (leqnn k). rewrite addnC. apply/eqP; rewrite eqn_add2r; apply/eqP. apply eq_bigl => i; by rewrite andbC -ltn_neqAle. Qed.
imports: mathcomp(all_ssreflect fingroup perm zmodp ssralg) ssr_ext f2