proposition: Lemma val2posE : val \o val2pos =1 nth (size t) s.
proof: Proof. Proof using. by []. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordcast partition Yamanouchi ordtype std tableau stdtab sorted Schensted congr plactic Greene Greene_inv