proposition: Lemma langQE u t : (u \in langQ t) = (RS (invstd (std u)) == t).
proof: Proof. by rewrite /langQ inE RSinvstdE. 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