proposition: Lemma extract_S1E : extract (in_tuple x) S1 = extract (in_tuple x) (S :&: [set j : 'I_(size x) | j <= posa]) ++ extract (in_tuple x) (T :&: [set j : 'I_(size x) | j > posc]).
proof: Proof. Proof using. rewrite /S1 /extract /= /extractpred (enumUltV (d := posa)). - 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