proposition: Lemma KostkaStd : Kostka la (colpartn d) = #|{: stdtabsh la}|.
proof: Proof. rewrite /Kostka. have -> : (mpart (colpartn d)) = [multinom (i < d)%N : nat | i < (size (colpartn d)).-1.+1]. apply/mnmP => /= i; rewrite /mpart. rewrite {2 3}size_colpartn leqSpred !mnmE. by rewrite {1}colpartnE nth_nseq; case: (ltnP i d). rewrite /KostkaMon /KostkaTab colpartnE size_nseq. rewrite -(card_imset _ (can_inj (tabord_of_natK (leqSpred _)))). apply eq_card => /= t; rewrite !inE. apply/eqP/imsetP => [Ht | [/= st _ ->{t}]]. - exists (tabnat_of_ord (leqSpred _) t); first by rewrite inE. by rewrite tabnat_of_ordK //= inE -Ht. - rewrite /= /tabord_of_nat_fun /= /tabnat_of_ord_fun /= to_word_map_tab. by rewrite stdtabsh_eval_to_word // leqSpred. 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