proposition: Lemma sum_num_occ_sub (k : 'I_#|A|) : sum_num_occ k.+1 - sum_num_occ k = N(enum_val k | ta).
proof: Proof. rewrite sum_num_occ_rec addnC; symmetry. by rewrite -{1}(addn0 N(enum_val k | ta)) -(subnn (sum_num_occ k)) addnBA. Qed.
imports: mathcomp(all_ssreflect fingroup perm zmodp ssralg) ssr_ext f2