proposition: Lemma changeUTK (disp : unit) (T : inhOrderType disp) (w : seq T) : (take d1 w) \in langQ U1 -> (drop d1 w) \in langQ U2 -> changeUT U1 U2 (changeUT T1 T2 w) = w.
proof: Proof. Proof using Hsh1 Hsh2. rewrite !inE /= /changeUT => /eqP Htake /eqP Hdrop. rewrite ?take_size_cat ?drop_size_cat ?size_RSmapinv2_yam //. have Htk : shape (RS (take d1 w)) = shape U1. by rewrite -RStabmapE shape_RStabmapE Htake. have Hdp : shape (RS (drop d1 w)) = shape U2. by rewrite -RStabmapE shape_RStabmapE Hdrop. have -> : RS (RSmapinv2 (RS (take d1 w), yam_of_stdtab T1)) = RS (take d1 w). by rewrite (toDepRSPair (changeTtakeP _)) -RStabE RStabinvK /=. have -> : RS (RSmapinv2 (RS (drop d1 w), yam_of_stdtab T2)) = RS (drop d1 w). by rewrite (toDepRSPair (changeTdropP _)) -RStabE RStabinvK /=. rewrite -{3}(cat_take_drop d1 w); congr (_ ++ _). - move: Htake; rewrite /RStabmap /= -!RSmapE. case H : (RSmap (take d1 w)) => [Pt Qt] <- /=. rewrite stdtab_of_yamK -/((Pt, Qt).2) -H; last exact: is_yam_RSmap2. by rewrite RSmapK. - move: Hdrop; rewrite /RStabmap /= -!RSmapE. case H : (RSmap (drop d1 w)) => [Pt Qt] <- /=. rewrite stdtab_of_yamK -/((Pt, Qt).2) -H; last exact: is_yam_RSmap2. by rewrite RSmapK. 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