proposition: Lemma tabsh_reading_RSP (sh : seq nat) (w : seq A) : reflect (exists tab, [/\ is_tableau tab, shape tab = sh & to_word tab = w]) (tabsh_reading_RS sh w).
proof: Proof. Proof using . apply (iffP idP). - move=> /andP[/eqP HRS /eqP Hsh]. exists (RS w); split => //; exact: is_tableau_RS. - move=> [tab] [Htab Hsh Hw]; apply/andP. have:= RS_tabE Htab; rewrite Hw => ->. by rewrite Hw Hsh. 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