proposition: Lemma size_partm m : size (partm m) <= n.
proof: Proof. rewrite partmE size_sort size_filter -[X in _ <= X](size_tuple m). exact: count_size. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm zmodp binomial) mathcomp(ssrcomplements freeg mpoly) tools permcomp presentSn sorted partition