proposition: Lemma mpart_is_dominant sh : is_part sh -> mpart sh \is dominant.
proof: Proof. rewrite /mpart /dominant; case: leqP => [Hsz|_ _]. - rewrite is_part_sortedE => /andP[Hpart _]. + apply/(sorted2P 0) => // i j; rewrite size_tuple => /andP[Hij Hj]. have Hi := leq_ltn_trans Hij Hj. rewrite -[i]/(val (Ordinal Hi)) -[j]/(val (Ordinal Hj)) -!mnm_nth !mnmE /=. case: (ssrnat.ltnP j (size sh)) => [Hjsz | /(nth_default _) -> //]. by apply: (sorted2P _ _ _ _ Hpart) => //; rewrite Hij Hjsz. - apply/(sorted2P 0) => // i j; rewrite size_tuple => /andP[Hij Hj] /=. by rewrite (nth_map (Ordinal Hj)) // -cardE card_ord. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm zmodp binomial) mathcomp(ssrcomplements freeg mpoly) tools permcomp presentSn sorted partition