proposition: Lemma KostkaMon_partdom m : KostkaMon m != 0 -> partdom m la.
proof: Proof. rewrite cards_eq0 => /set0Pn [/= t]; rewrite inE => /eqP <-. exact: tab_eval_partdom. 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