proposition: Lemma shape_bij_LRsupport : shape bij_LRsupport = shape Q.
proof: Proof. Proof using HTriple Hsh1 Hsh2. have:= take_drop_langQ; rewrite /= -shape_RStabmapE RStabmapE. rewrite !inE => [] [/eqP HU1 /eqP HU2]. have -> : RS (changeUT T1 T2 w) = RS w. apply/eqP; rewrite -plactic_RS; by apply: plact_changeUT; rewrite -RStabmapE shape_RStabmapE ?HU1 ?HU2. rewrite /w -RSmapE shape_RSmap_eq /w RSmapinv2K; last exact: RSpairyamQ. by rewrite //= shape_yam_of_stdtab. 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