proposition: Lemma mpart0 : @mpart [::] = 0%MM.
proof: Proof. by apply mnmP => i; rewrite /mpart /= mnmE mnm0E 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