proposition: Fact partmP m : is_part (sort geq [seq d <- m | d != 0]).
proof: Proof. rewrite is_part_sortedE; apply/andP; split. - exact: sort_sorted. - by rewrite mem_sort mem_filter eq_refl. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm zmodp binomial) mathcomp(ssrcomplements freeg mpoly) tools permcomp presentSn sorted partition