proposition: Lemma size_langQ t u : u \in langQ t -> size u = size_tab t.
proof: Proof. Proof using . rewrite langQE => /eqP <-. by rewrite -size_RS -RStabmapE RSinvstdE /size_tab shape_RStabmapE. 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