proposition: Lemma KostkaMon_sumeval m : mdeg m != sumn la -> KostkaMon m = 0.
proof: Proof. move=> H; apply/eqP; move: H. apply contraR; rewrite cards_eq0 => /set0Pn /= [t]. rewrite /mdeg -sumnE inE => /eqP <-{m}. by rewrite sumn_eval size_to_word /size_tab shape_tabsh. 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