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