proposition: Lemma sum_num_occ_is_enum_val (k : 'I_#|A|) (l : 'I_n) : sum_num_occ k <= l < sum_num_occ k.+1 = (ta!_l == enum_val k).
proof: Proof. case/boolP : (sum_num_occ k <= l < sum_num_occ k.+1) => Hcase. - exact/esym/eqP/sum_num_occ_enum_val. - apply/esym/negbTE;apply: contra Hcase => /eqP; exact: enum_val_sum_num_occ. Qed.
imports: mathcomp(all_ssreflect fingroup perm zmodp ssralg) ssr_ext f2