proposition: Lemma add_mesymE : size la <= n -> #|h| == k -> ~~ hasincr -> mpart add_mesym = (mpart la + mesym1 h)%MM.
proof: Proof. Proof using . rewrite /add_mesym /add_mpart_mesym => Hsz /= /eqP <- Hincr. rewrite /mpart Hincr Hsz eq_refl /=. set S := (map _ _). rewrite mnmP => i. rewrite (leq_trans (size_rem_trail0 S)); last by rewrite size_map size_enum_ord. rewrite mnmE nth_rem_trail0. have H0 : 0 < n by apply: (leq_ltn_trans _ (ltn_ord i)). rewrite !(nth_map (Ordinal H0) 0) ?size_enum_ord // !mnmE. by rewrite !nth_ord_enum. 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