proposition: Lemma plact_changeUT_take : take d1 (changeUT T1 T2 w) =Pl take d1 w.
proof: Proof. Proof using Hsh1 Htake. rewrite /changeUT take_size_cat; last by rewrite /= size_RSmapinv2_yam. rewrite (toDepRSPair changeTtakeP). apply Sch_plact; apply/eqP. by rewrite -[LHS]RStabE RStabinvK //. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg) mathcomp(ssrcomplements freeg mpoly) tools ordtype partition Yamanouchi std tableau stdtab Schensted congr plactic stdplact Yam_plact Greene_inv shuffle Schur_mpoly