proposition: Lemma take_drop_langQ : ((take d1 w) \in langQ U1 /\ (drop d1 w) \in langQ U2).
proof: Proof. Proof using HTriple. have:= HTriple => /LRtripleP-/(_ (stdtabnP _) (stdtabnP _)) Htriple. have Hszw : size w = (d1 + d2)%N by rewrite /w size_RSmapinv2_yam. rewrite LRtriple_cat_equiv //; split. - rewrite size_take size_tab_stdtabn Hszw. case: d2 => [| n]; first by rewrite addn0 ltnn. by rewrite addnS ltnS leq_addr. - by rewrite size_drop size_tab_stdtabn Hszw addKn. - exists (val Q); split; first exact: Htriple. rewrite cat_take_drop /w inE /= /RStabmap RSmapinv2K; last exact: RSpairyamQ. by rewrite yam_of_stdtabK. 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