proposition: Lemma plact_changeUT : changeUT T1 T2 w =Pl w.
proof: Proof. Proof using Hdrop Hsh1 Hsh2 Htake. rewrite /changeUT -{3}(cat_take_drop d1 w). apply: plact_cat. - have:= plact_changeUT_take. by rewrite /changeUT take_size_cat // size_RSmapinv2_yam. - have:= plact_changeUT_drop. by rewrite /changeUT drop_size_cat // size_RSmapinv2_yam. 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