proposition: Lemma size_mpart_in_supp (f : {mpoly R[n]}) d (p : 'P_d) : f \is d.-homog -> mpart p \in msupp f -> size p <= n.
proof: Proof. rewrite /mpart; case: leqP => //= H1 /dhomogP H{}/H /=. rewrite /= mdeg0 => Hd; subst d. by move: H1; rewrite intpartn0 size_rowpartn. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm) mathcomp(ssrcomplements freeg mpoly) sorted tools ordtype permuted partition skewpart composition Yamanouchi std tableau stdtab skewtab permcent antisym Schur_mpoly therule Schur_altdef unitriginv