proposition: Lemma sum_num_occ_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. move: (ltnSn k). set k':= {2}k.+1. move: k' => k'. elim: k' l k => [l k /= | m IH l k km]; first by rewrite ltn0. case/boolP : (k < m) => Hcase; first by apply IH. rewrite -leqNgt in Hcase. have : m = k by apply/eqP; rewrite eqn_leq; apply/andP. rewrite {Hcase} => ?; subst m. case/andP => [Hlm1 Hlm2]. apply/eqP/negPn/negP; move=> abs. case/boolP : (lt_rank ta!_l (enum_val k)) => Hcase. - have Hrank : enum_rank ta!_l < k by rewrite lt_rank_alt enum_valK in Hcase. have Hcontr : #|[set i | (i==l) || (sum_num_occ (enum_rank ta!_l)<= i < sum_num_occ (enum_rank ta!_l).+1)]| <= N(ta!_l|ta). rewrite num_occ_alt subset_leq_card // subsetE; apply/pred0P => i /=. rewrite !in_set /=. apply/negbTE; rewrite negb_and. case/boolP : (ta!_i == ta!_l) => ta_il //. rewrite negb_or; apply/andP; split. - move: ta_il; apply contra => /eqP ->; by rewrite eqxx. - move: ta_il; apply contra => ta_il. apply/eqP; rewrite -(enum_rankK (ta!_l)); by apply IH. rewrite (_ : #|[set i | (i == l) || (sum_num_occ (enum_rank ta!_l) <= i < sum_num_occ (enum_rank ta!_l).+1)]| = N(ta!_l | ta).+1) in Hcontr; first by rewrite ltnn in Hcontr. 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 (enum_rank ta!_l)) N(enum_val (enum_rank ta!_l) | ta)]) 1); last first. apply eq_bigl => i; rewrite !in_set. case/boolP : (i != l) => Hcase2. - rewrite mem_iota. move/negPf in Hcase2; by rewrite andbT Hcase2 orFb. - rewrite negbK in Hcase2; move/eqP in Hcase2; subst i. rewrite andbF mem_iota. apply/negP; case/andP => H1. rewrite -sum_num_occ_rec; apply/negP; rewrite -leqNgt. by rewrite (leq_trans _ Hlm1) // sum_num_occ_inc. by rewrite sum1_card set_predleq_size enum_rankK // -{2}(enum_rankK ta!_l) -sum_num_occ_rec sum_num_occ_leq_n. - have {abs} {}Hcase : lt_rank (enum_val k) ta!_l. rewrite lt_rank_alt; rewrite lt_rank_alt -leqNgt in Hcase. rewrite ltn_neqAle; apply/andP; split => //. rewrite enum_valK. suff : k != enum_rank ta!_l by move=> ->. apply/negP ; move/eqP. move=> abs2; symmetry in abs2; rewrite -abs2 enum_rankK {abs2} in abs. contradict abs ; by apply/negP/negPn/eqP. move/negP : (ltnn N(enum_val k | ta)) => abs; contradict abs. rewrite {1}num_occ_alt. have H : #|[set i | ta!_i == enum_val k]| <= #|[set i : 'I_n | (sum_num_occ k <= i < l)]|. apply subset_leq_card. rewrite subsetE; apply/pred0P => i /=. rewrite !in_set /=. apply/negP/negP. rewrite negb_and negbK. case/boolP : (sum_num_occ k <= i < l) => Hcase2; first by apply/orP; apply or_introl. case/boolP : (l <= i) => Hcase3. + rewrite eq_sym; apply lt_neq_rank. eapply lt_le_rank_trans; first by apply Hcase. apply sorted_of_tnth_leq => //; [exact/le_rank_trans | exact/le_rank_refl]. + rewrite -ltnNge in Hcase3. rewrite Hcase3 andbT -ltnNge {Hcase3} in Hcase2. apply lt_neq_rank. have lt0m : 0 < k. rewrite ltnNge leqn0 ; apply/eqP => abs2. contradict Hcase2 ; by rewrite abs2 sum_num_occ_0 ltn0. have H2 : forall (k' : 'I_#|A|) (l : 'I_n), k'.-1 < k -> l < sum_num_occ k' -> lt_rank ta!_l (enum_val k'). case; elim. - move=> H0 l0 /= _ abs2 ; contradict abs2 ; by rewrite sum_num_occ_0 ltn0. - move=> k' HR' HSk l0 /= k'k Hl0. have Hk' : k' < #|A| by apply: (leq_trans k'k _); apply ltnW. apply: (@le_lt_rank_trans _ _ (enum_val (Ordinal Hk'))). - case/boolP : (l0 < sum_num_occ k') => Hcase3; rewrite /le_rank leq_eqVlt; apply/orP; [apply or_intror | apply or_introl]. - rewrite -lt_rank_alt; apply HR'; by [apply: (leq_ltn_trans (leq_pred _) k'k) | apply Hcase3]. - rewrite -leqNgt in Hcase3; rewrite (IH _ (Ordinal Hk')) //; by apply/andP. - rewrite lt_rank_alt !enum_valK; by apply ltnSn. apply H2 ; by [rewrite -{2}(prednK lt0m) ; apply ltnSn | apply Hcase2]. rewrite -(subnKC Hlm1) in H. set lhs := #| _ | in H. have {}H : lhs <= #|[set i : 'I_n | nat_of_ord i \in iota (sum_num_occ k) (l - sum_num_occ k)]|. apply (leq_trans H), eq_leq. by apply eq_card => /= i; rewrite !inE mem_iota. rewrite set_predleq_size in H; last by rewrite (subnKC Hlm1) ltnW. apply: (leq_ltn_trans H _). by rewrite -sum_num_occ_sub /= ltn_sub2r // (leq_ltn_trans Hlm1 Hlm2). Qed.
imports: mathcomp(all_ssreflect fingroup perm zmodp ssralg) ssr_ext f2