proposition: Lemma mpartS n mu : size mu <= n -> mnmwiden (mpart n mu) = mpart n.+1 mu.
proof: Proof. case: n => [|n]. rewrite leqn0 => /eqP; case: mu => //= _. rewrite /mpart /=. suff Hm0 (n) : [multinom nth 0 [::] i | i < n] = 0%MM. by rewrite !Hm0 mnmwiden0. by apply/mnmP => i; rewrite !mnmE nth_default. move => H. rewrite /mpart H. have:= H; rewrite -ltnS => /ltnW ->. apply mnmP => i; rewrite /mnmwiden. rewrite (mnm_nth 0) /= nth_rcons size_map size_enum_ord if_same mnmE. case: ssrnat.ltnP => Hi. - by rewrite (nth_map ord0) ?nth_enum_ord ?size_enum_ord. - by rewrite nth_default //; apply: (leq_trans H Hi). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm) mathcomp(mpoly) tools combclass ordtype sorted partition tableau skewpart skewtab antisym Schur_mpoly freeSchur therule std stdtab unitriginv presentSn