proposition: Lemma extract_swap_set_S : sorted R (extract (in_tuple x) (swap_set S)).
proof: Proof. Proof using HRabc HS HbNin Hposa Hposc Px. rewrite extract_swap_setSE. have : sorted R (extract (in_tuple x) S). move: Px => /and3P[_ _ /forallP Hall]. by have := Hall S; rewrite HS. rewrite extract_SE. set LL := extract _ _; set LR := extract _ _; rewrite /= => Hsort. have HacR := subseq_sorted (Rtrans HRabc) (suffix_subseq _ _) Hsort. have HbcR : sorted R [:: b, c & LR]. by move: HacR; rewrite /= (Hbc HRabc)=> /andP[_ ->]. case: LL Hsort => //= LL0 LL. rewrite !cat_path => /andP[-> /= /and3P[/(Hxba HRabc) -> _ ->]]. by rewrite (Hbc HRabc). Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools ordcast ordtype subseq partition tableau Yamanouchi stdtab Schensted congr plactic Greene