proposition: Lemma enum_val_sum_num_occ (k : 'I_#|A|) (l : 'I_n) : ta!_l = enum_val k -> sum_num_occ k <= l < sum_num_occ k.+1.
proof: Proof. move=> Hkl; apply/negP => /negP abs. have : #|[set i | (i == l) || (sum_num_occ k <= i < sum_num_occ k.+1)]| <= N(ta!_l | ta). rewrite num_occ_alt subset_leq_card // subsetE. apply/pred0P => /= i /=; rewrite !in_set /=. case/boolP : (ta!_i == ta!_l) => ta_il //=. apply/negbTE; rewrite negb_or; apply/andP; split. - move: ta_il; apply: contra => /eqP ?; subst l; by rewrite eqxx. - move: ta_il; apply: contra => Hsum_num_occ. apply/eqP; rewrite Hkl; by apply sum_num_occ_enum_val. suff -> : #|[set i | (i == l) || (sum_num_occ k <= i < sum_num_occ k.+1)]| = N(ta!_l | ta).+1. by rewrite ltnn. symmetry; rewrite -addn1 sum_num_occ_rec -sum1_card. rewrite (bigD1 l) /=; last by rewrite in_set; apply/orP; apply or_introl. rewrite addnC; apply/eqP; rewrite eqn_add2l; apply/eqP. transitivity ( \sum_(i in [set i0 : 'I_n | nat_of_ord i0 \in iota (sum_num_occ k) N(enum_val k | ta)]) 1 ). rewrite sum1_card set_predleq_size; by [rewrite Hkl | rewrite -sum_num_occ_rec; apply sum_num_occ_leq_n]. apply eq_bigl => i; rewrite !in_set. case/boolP : (i != l) => [/negPf |] il. - by rewrite andbT il orFb mem_iota. - rewrite negbK in il; move/eqP in il; subst i. rewrite andbF mem_iota. apply/negbTE; move: abs; apply contra. by rewrite -sum_num_occ_rec. Qed.
imports: mathcomp(all_ssreflect fingroup perm zmodp ssralg) ssr_ext f2