proposition: Lemma add_mesymK d k (la : 'P_d) : size la <= n -> {in [pred mu : 'P_(d + k) | vb_strip la mu && (size mu <= n)], cancel (fun mu : 'P_(d + k) => setdiff la (val mu)) (add_mesym k la)}.
proof: Proof. Proof using . move=> Hszla mu /=; rewrite inE => /andP[Hstrip Hsz]. have:= vb_stripP (intpartnP _) (intpartnP _) Hstrip => Hstr. apply/eqP/(part_eqP (intpartnP _) (intpartnP _)) => i. rewrite /add_mesym /=. rewrite Hszla card_setdiff // eq_refl /= nohasincr_setdiff //. by rewrite nth_rem_trail0 nth_add_setdiff. 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