proposition: Lemma tabword_of_tuple_freeSchur_inj (Q : stdtabn d) : {in (freeSchur Q) &, injective tabword_of_tuple}.
proof: Proof. Proof using . move=> /= u v. rewrite /freeSchur !inE => /eqP Hu /eqP Hv /(congr1 (@tval _ _)) /= H. case: (bijRStab 'I_n) => RSinv HK _. apply: val_inj; rewrite -[val u]HK -[val v]HK; congr (RSinv _). rewrite {RSinv HK} /RStab /=. apply: pqpair_inj => /=. have:= (is_tableau_RS u). have:= is_tableau_RS v. move: Hu Hv H; rewrite -!RStabmapE /RStabmap. case: RSmap => [pu qu] /= ->; case: RSmap => [pv qv] /= -> Heq Hv Hu. by rewrite -(RS_tabE Hu) -(RS_tabE Hv) Heq. 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