proposition: Lemma cat_tuple_inj d1 d2 (u x : d1.-tuple 'I_n) (v y : d2.-tuple 'I_n) : cat_tuple u v = cat_tuple x y -> (u, v) = (x, y).
proof: Proof. Proof using . rewrite /cat_tuple => [] [/eqP]. rewrite eqseq_cat; last by rewrite !size_tuple. by move=> /andP[/eqP/val_inj -> /eqP/val_inj ->]. 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