proposition: Lemma size_RS_tuple (t : d.-tuple 'I_n) : size (to_word (RS t)) == d.
proof: Proof. Proof using . by rewrite size_to_word -{2}(size_tuple t) size_RS. 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