proposition: Lemma add_mpart_mesymP : is_part_of_n (d + k) add_mpart_mesym.
proof: Proof. Proof using la h. rewrite /add_mpart_mesym. case: (boolP [&& _, _ & _]) => [/and3P[Hsz /eqP<- Hincr] | _]. - exact: not_hasincr_part. - by rewrite rowpartnE; apply: rowpartn_subproof. 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