proposition: Lemma Kostka0 (la mu : 'PDom_d) : ~~ (mu <= la)%O -> 'K(la, mu) = 0.
proof: Proof. by move=> H; apply/eqP; move: H; apply contraR; apply Kostka_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