proposition: Lemma is_dominant_partm m : m \is dominant -> partm m = [seq d <- m | d != 0] :> seq nat.
proof: Proof. rewrite unfold_in partmE => Hsort. apply: (sorted_eq (leT := geq)) => //. - exact: sort_sorted. - exact: sorted_filter. - by rewrite perm_sort. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm zmodp binomial) mathcomp(ssrcomplements freeg mpoly) tools permcomp presentSn sorted partition