proposition: Lemma extract_T1 : sorted R (extract (in_tuple x) T1).
proof: Proof. Proof using HRabc HS HT Hposb Hposc Px. move: Px => /and3P[_ _ /forallP Hall]. rewrite extract_T1E; set lL := (X in X ++ _); set lR := (X in _ ++ X). have:= Hall S; rewrite HS => /= HseqS. have:= Hall T; rewrite HT => /= HseqT {Hall}. have : sorted R lR by apply: (sorted_extract_cond (Rtrans HRabc) _ HseqS). have : sorted R lL by apply: (sorted_extract_cond (Rtrans HRabc) _ HseqT). rewrite /=; case HlL: lL => [|l0 lL']; first by rewrite cat0s. rewrite /sorted /= cat_path => -> /=. rewrite /lR extract_cS /= => ->; rewrite andbT. have -> : last l0 lL' = b. have := extract_Tb; rewrite -/lL HlL. by case: (extract _ _) => [| y z] [-> ->]; last rewrite last_rcons. exact: (Hbc HRabc). Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools ordcast ordtype subseq partition tableau Yamanouchi stdtab Schensted congr plactic Greene