proposition: Lemma mpartE s i : size s <= n -> mpart s i = nth 0 s i.
proof: Proof. by rewrite /mpart => ->; rewrite mnmE. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm zmodp binomial) mathcomp(ssrcomplements freeg mpoly) tools permcomp presentSn sorted partition