proposition: Lemma extract_swap_set T : T != swap_set S -> T \in Qbnotin -> sorted R (extract (in_tuple x) T).
proof: Proof. Proof using HS HbNin Hposa Px. move/inPQE => /[apply] HT; move: Px => /and3P[_ _ /forallP/(_ T)]. by rewrite HT. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools ordcast ordtype subseq partition tableau Yamanouchi stdtab Schensted congr plactic Greene