proposition: Lemma index_invstd l i : is_std l -> i < size l -> index i (invstd l) = nth inh l i.
proof: Proof. Proof using . move=> Hstd Hi. by rewrite -{2}(invstdK Hstd) /invstd nth_mkseq //= size_mkseq. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype finfun fintype choice) mathcomp(order seq tuple finset perm binomial bigop) tools vectNK subseq partition Yamanouchi ordtype std tableau stdtab Schensted plactic Greene_inv stdplact