proposition: Lemma is_dominant_nth_partm m (i : 'I_n) : m \is dominant -> nth 0 (partm m) i = m i.
proof: Proof. move=> Hdom; rewrite (is_dominant_partm Hdom). case: m Hdom => [[s Hs /=]]. rewrite unfold_in (mnm_nth 0) /=. case: i => [i /= _] {Hs}; elim: s i => [| s0 s IHs] i // Hsort /=. case: (s0 =P 0) Hsort => [->{s0} /= {IHs} Hpath | _]. - have -> : s = nseq (size s) 0. elim: s Hpath => //= s0 s IHs /andP[]. by rewrite leqn0 => /eqP-> /IHs {1}->. rewrite (eq_in_filter (a2 := pred0)) ?filter_pred0; first last. by move=> x /nseqP[-> _]. by case: i => //= i; rewrite nth_nseq if_same. - move=> /sorted_consK {}/IHs /= Hrec. by case: i. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm zmodp binomial) mathcomp(ssrcomplements freeg mpoly) tools permcomp presentSn sorted partition