proposition: Lemma sumn_mpart sh : size sh <= n -> sumn (mpart sh) = sumn sh.
proof: Proof. move=> Hsz; rewrite /mpart Hsz !sumnE big_tuple. under [LHS]eq_bigr do rewrite tnth_mktuple. rewrite (big_nth 0) big_mkord (big_ord_widen _ _ Hsz). rewrite (bigID (fun i : 'I_n => i < size sh)) /= addnC big1 ?add0n //. by move=> i; rewrite -leqNgt; apply: nth_default. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm zmodp binomial) mathcomp(ssrcomplements freeg mpoly) tools permcomp presentSn sorted partition