proposition: Lemma mpart_partm_perm m : {s : 'S_n | (mpart (partm m)) == m # s}.
proof: Proof. have [/= s /eqP {2}<-]:= perm_mpart_partm m. exists (s^-1); apply/eqP/mnmP => i. by rewrite 2!mnmE permKV. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm zmodp binomial) mathcomp(ssrcomplements freeg mpoly) tools permcomp presentSn sorted partition