proposition: Lemma partm_permK m : perm_eq m (mpart (partm m)).
proof: Proof. have Hsm : size (sort geq m) == n by rewrite size_sort size_tuple. pose sm := [multinom Tuple Hsm]. have Hperm : perm_eq sm m by rewrite /= perm_sort. rewrite -(perm_partm Hperm) partmK; first last. by rewrite unfold_in; apply: sort_sorted. by rewrite perm_sym. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm zmodp binomial) mathcomp(ssrcomplements freeg mpoly) tools permcomp presentSn sorted partition