proposition: Lemma partmK m : m \is dominant -> mpart (partm m) = m.
proof: Proof. move=> Hdom; rewrite /mpart size_partm. by apply/mnmP => i; rewrite mnmE is_dominant_nth_partm. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm zmodp binomial) mathcomp(ssrcomplements freeg mpoly) tools permcomp presentSn sorted partition