proposition: Lemma shape_takeRS : shape (RS (take d1 w)) = shape U1.
proof: Proof. Proof using HTriple. have:= take_drop_langQ; rewrite -/w => /= [] [Htake _]. move: Htake; rewrite inE => /eqP <-. by rewrite -RStabmapE shape_RStabmapE. 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