proposition: Lemma Kostka_diag la : 'K(la, la) = 1.
proof: Proof. case Hla : (size la) => [|szla]. rewrite /Kostka /KostkaMon Hla. move: Hla => /eqP/nilP Hla. have {Hla} Hd : d = 0 by rewrite -(sumn_intpartn la) Hla. subst d. have Ht : is_tab_of_shape la ([::] : seq (seq 'I_1)) by rewrite val_intpartn0. rewrite [KostkaTab _ _](_ : _ = [set TabSh Ht]) ?cards1 //. apply/setP => t; rewrite !inE; apply/eqP/eqP => [|->]/=. - rewrite /mpart val_intpartn0 /= => /(congr1 (fun t : 1.-tuple nat => sumn t)). rewrite sumn_eval size_to_word /=. rewrite (map_comp _ nat_of_ord) val_enum_ord /= addn0. by move=> /(tab0 (tabshP _)) => Ht0; apply val_inj. - rewrite /to_word /=; apply eq_from_tnth => i. by rewrite /mpart val_intpartn0 /= !tnth_mktuple /=. rewrite (Kostka_any la (n := szla)) /KostkaMon ?Hla //. have Hntht j : nth [::] [seq nseq (nth 0 la (i : nat)) i | i : 'I_szla.+1] j = nseq (nth 0 la j) (inord j). case: (ssrnat.ltnP j szla.+1) => Hj. - rewrite (nth_map ord0) ?size_enum_ord // nth_enum_ord //. by congr nseq; apply val_inj; rewrite /= inordK // nth_enum_ord. - by rewrite !nth_default ?Hla // size_map size_enum_ord. have Hleqla : size la <= szla.+1 by rewrite Hla. rewrite [KostkaTab _ _](_ : _ = [set tabrowconst Hleqla]) ?cards1 //. apply/setP => /= t; rewrite !inE; apply/eqP/eqP => [|->]/=. - rewrite /mpart Hla ltnSn => H. apply/eqP/tab_eqP; rewrite ?tabshP // => // /= i. rewrite take_oversize; last by rewrite size_map size_enum_ord -Hla. rewrite {}Hntht. have Hsht := shape_tabsh t. elim: i.+1 {-2}i (ltnSn i) => {i} [//| i IHi] j. rewrite ltnS leq_eqVlt => /orP[/eqP->{j}|]; last exact: IHi. have Hszt : size t = szla.+1. by rewrite -(size_map size) -/(shape t) Hsht Hla. case: (ssrnat.ltnP i (size la)) => Hi; first last. by rewrite !nth_default // Hszt -Hla. rewrite Hla in Hi. rewrite -Hsht nth_shape; apply/all_pred1P; rewrite all_count -nth_shape Hsht. have:= congr1 (fun t => tnth t (inord i)) H. rewrite /eval !tnth_mktuple inordK // => <-. rewrite /to_word seq.count_flatten map_rev sumn_rev sumnE big_map. rewrite (big_nth [::]) Hszt big_mkord. rewrite (bigD1 (inord i)) //= inordK // big1 ?addn0 //. move=> j Hj. case: (ssrnat.ltnP j i) => [/IHi -> | Hij]. - rewrite count_nseq /= inord_val. by move: Hj => /negbTE ->; rewrite mul0n. - have {Hi}Hij : i < j. rewrite ltn_neqAle Hij andbT. by move: Hj; apply contra => /eqP ->; rewrite inord_val. rewrite (eq_in_count (a2 := pred0)) ?count_pred0 // => /= x. rewrite eq_sym /eq_op /= (inordK (ltn_trans Hij _)) //. by move=> /(allP (all_ltn_nth_tabsh _ _)) /(leq_trans Hij) /ltn_eqF ->. - apply eq_from_tnth => i. rewrite take_oversize; last by rewrite size_map size_enum_ord -Hla. rewrite /eval /mpart Hla ltnSn !tnth_mktuple. rewrite /to_word seq.count_flatten map_rev sumn_rev -map_comp. rewrite sumnE big_map enumT -/(index_enum _) (bigD1 i) //=. rewrite big1 ?addn0 ?count_nseq /= ?eq_refl ?mul1n //. move=> j Hj; apply/count_memPn/nseqP => [] [Heq _]. by rewrite Heq eq_refl in Hj. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm) mathcomp(mpoly) tools combclass ordtype sorted partition tableau skewpart skewtab antisym Schur_mpoly freeSchur therule std stdtab unitriginv presentSn