proposition: Corollary RS_yam_RS y : is_yam y -> RS y = yamtab (shape (RS y)).
proof: Proof. move=> Hyam. exact (yamtab_unique (is_tableau_RS y) (is_yam_plactic Hyam (congr_RS y))). 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