proposition: Lemma Kostka_sumnE la mu : d != sumn mu -> Kostka la mu = 0.
proof: Proof. rewrite /Kostka => Hd; apply KostkaMon_sumeval. by rewrite eq_sym sumn_intpartn mdeg_mpart ?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