proposition: Lemma full_sum_num_occ (k : nat) : #|A| <= k -> sum_num_occ k = \sum_(i < #|A|) N(enum_val i | ta).
proof: Proof. move=> Hk; apply eq_bigl => i; by rewrite (leq_trans (ltn_ord i) Hk). Qed.
imports: mathcomp(all_ssreflect fingroup perm zmodp ssralg) ssr_ext f2