proposition: Lemma shape_RS_yam y : is_yam y -> shape (RS y) = evalseq y.
proof: Proof. move => Hyam. have:= congr_RS y => /plact_homog. rewrite perm_evalseq => /eqP ->. rewrite {2}(RS_yam_RS Hyam) to_word_yamtab evalseq_hyper_yam //=. by apply is_part_sht; exact: is_tableau_RS. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(tuple finfun finset path bigop order) tools partition Yamanouchi ordtype std tableau stdtab Schensted congr plactic Greene_inv stdplact