proposition: Lemma to_word_yamtab sh : to_word (yamtab sh) = hyper_yam sh.
proof: Proof. elim/last_ind: sh => [//= | sh sn] /=. have -> : yamtab (rcons sh sn) = rcons (yamtab sh) (nseq sn (size sh)). rewrite /yamtab -[size sh]add0n; move: 0. elim: sh => [//= | s0 sh IHsh] /= i; first by rewrite addn0. by rewrite IHsh addSnnS. rewrite /hyper_yam to_word_rcons rev_rcons /= => ->. by rewrite size_rev. 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