proposition: Lemma mdeg_mpart sh : size sh <= n -> mdeg (mpart sh) = sumn sh.
proof: Proof. by move/sumn_mpart => <-; rewrite sumnE -/(mdeg _). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm zmodp binomial) mathcomp(ssrcomplements freeg mpoly) tools permcomp presentSn sorted partition