proposition: Lemma Kostka_partdom (la mu : 'PDom_d) : 'K(la, mu) != 0 -> (mu <= la)%O.
proof: Proof. rewrite /Kostka => /KostkaMon_partdom. rewrite /mpart leqSpred => /partdomP Hdom. apply/partdomP => i; move/(_ i): Hdom; congr (_ <= _). rewrite !sumn_take; apply eq_bigr => {}i _. case: (ssrnat.ltnP i (size mu)) => Hi. - have -> : (size mu).-1.+1 = (size mu) by case: (size mu) Hi. by rewrite -{1}[i]/((Ordinal Hi) : nat) -mnm_nth mnmE. - rewrite [RHS]nth_default //. case: mu Hi => [[|m mu] Hmu] Hi. + case: i Hi => [|i]. * by rewrite -[X in nth _ _ X]/((@ord0 0) : nat) -mnm_nth mnmE. * by rewrite nth_default //= size_tuple card_ord. + move: Hmu Hi; rewrite /= => _ => Hi. by rewrite nth_default // size_tuple card_ord. 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