proposition: Lemma mpartK sh : is_part sh -> size sh <= n -> partm (mpart sh) = sh :> seq nat.
proof: Proof. move=> Hpart Hsize; apply/eqP/part_eqP => // i. case: (ssrnat.ltnP i n) => Hi. - have /is_dominant_nth_partm Hdom := mpart_is_dominant Hpart. have:= Hdom (Ordinal Hi) => /= ->. by rewrite /mpart Hsize mnmE /=. - rewrite !nth_default //; apply: leq_trans _ Hi => //. exact: size_partm. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm zmodp binomial) mathcomp(ssrcomplements freeg mpoly) tools permcomp presentSn sorted partition