proposition: Lemma partmE m : partm m = sort geq [seq d <- m | d != 0] :> seq nat.
proof: Proof. by rewrite /partm; unlock. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm zmodp binomial) mathcomp(ssrcomplements freeg mpoly) tools permcomp presentSn sorted partition