proposition: Lemma Kostka_size0 la mu : size la > size mu -> 'K(la, mu) = 0.
proof: Proof. move=> H; apply/eqP; move: H. case Hsz : (size mu) => [|sz] /=. move=> Hla; rewrite cards_eq0 Hsz /=. move: Hsz => /eqP/nilP ->. rewrite -subset0; apply/subsetP => t; rewrite !inE. move=> /eqP/(congr1 (fun t : _.-tuple nat => sumn t)). rewrite sumn_eval size_to_word sumn_mpart //= => /(tab0 (tabshP _)) Ht. by move: Hla; rewrite -(shape_tabsh t) size_map Ht. apply contraLR; rewrite cards_eq0 -leqNgt => /set0Pn /= [t _]. have := size_tabsh t. by rewrite -(shape_tabsh t) size_map [X in _ <= X.-1.+1]Hsz /=. 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