proposition: Lemma perm_partm m1 m2 : perm_eq m1 m2 -> partm m1 = partm m2.
proof: Proof. move=> Hperm; apply val_inj; rewrite /= !partmE; apply/perm_sortP => //. exact: perm_filter. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm zmodp binomial) mathcomp(ssrcomplements freeg mpoly) tools permcomp presentSn sorted partition