proposition: Lemma extract_T1E : extract (in_tuple x) T1 = extract (in_tuple x) (T :&: [set j : 'I_(size x) | j <= posb]) ++ extract (in_tuple x) (S :&: [set j : 'I_(size x) | j >= posc]).
proof: Proof. Proof using. rewrite /T1 /extract /= /extractpred (enumUltV (d := posb)). - by rewrite map_cat. - by move=> i; rewrite !inE => /andP[_ Hi]. - move=> i; rewrite !inE => /andP[_ Hi] /=. exact: (ltn_trans (ltnSn _)). Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools ordcast ordtype subseq partition tableau Yamanouchi stdtab Schensted congr plactic Greene