proposition: Lemma perm_mpart s1 s2 : perm_eq s1 s2 -> perm_eq (mpart s1) (mpart s2).
proof: Proof. move=> Hperm; have Hsz := perm_size Hperm; rewrite /mpart -Hsz. case: leqP => Hszle; last exact: perm_refl. apply/seq.permP => P. have H s : size s <= n -> count P [multinom nth 0 s i | i < n] = count P s + \sum_(i < n | (P 0) && ~~(i < size s)) 1. move=> {}Hsz. rewrite -!sum1_count /= big_map enumT -/(index_enum _). rewrite (bigID (fun i : 'I_n => i < size s)) /=; congr (_ + _). - rewrite (big_nth 0) big_mkord. by rewrite (big_ord_widen_cond n (fun i => P (nth 0 s i)) (fun => 1)). - apply eq_bigl => i; rewrite [LHS]andbC [RHS]andbC. by case: (ssrnat.ltnP i (size s)) => //= H; rewrite nth_default. by rewrite !{}H -?Hsz // -(seq.permP Hperm). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm zmodp binomial) mathcomp(ssrcomplements freeg mpoly) tools permcomp presentSn sorted partition