proposition: Lemma Kostka_any la mu n : size mu <= n.+1 -> 'K(la, mu) = KostkaMon la (mpart n.+1 mu).
proof: Proof. rewrite /Kostka => Hsz. case: (size mu =P n.+1) => [-> //=| /eqP/negbTE H]. have {H}Hsz : size mu <= n. by move: Hsz; rewrite leq_eqVlt H /= ltnS. rewrite -(subnKC Hsz). elim: (n - size mu) => {n Hsz}[|n ->] /=. rewrite addn0; have := mpartS (leqnn (size mu)). by case: (size mu) => //= n; rewrite Kostka_mnmwiden => ->. rewrite Kostka_mnmwiden addnS; congr KostkaMon. rewrite /mpart -addnS; symmetry; rewrite -{2}addnS !leq_addr !addnS. apply mnmP => i; rewrite /mnmwiden !mnmE. rewrite (mnm_nth 0) /= nth_rcons size_map size_enum_ord if_same. case: ssrnat.ltnP => Hi. - by rewrite (nth_map ord0) ?nth_enum_ord // size_enum_ord. - by apply nth_default; apply: (leq_trans _ (ltnW Hi)); apply leq_addr. 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