proposition: Theorem yam_plactic_hyper y : is_yam y -> y =Pl hyper_yam (evalseq y).
proof: Proof. move => Hyam; rewrite -(shape_RS_yam Hyam) -to_word_yamtab. have HPly := congr_RS y. by rewrite -(yamtab_unique (is_tableau_RS y) (is_yam_plactic Hyam HPly)). 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