proposition: Lemma extract_SE : extract (in_tuple x) S = (extract (in_tuple x) (S :&: [set j : 'I_(size x) | j < size u])) ++ a :: c :: extract (in_tuple x) (S :&: [set j : 'I_(size x) | (size u).+2 < j]).
proof: Proof. Proof using HS HbNin Hposa Hposc. rewrite (extract_cut (in_tuple x) Hposa) /= Swap.tnth_pos1. rewrite (_ : setI _ _ = S :&: [set j : 'I_(size x) | j < size u]); first last. rewrite -!setIdE -setP => i; rewrite !inE. case: (ltnP i (size u)) => Hi; first by rewrite (ltn_trans Hi). case: (ltnP i (size u).+1) => Hi2; last by rewrite andbF. have -> : i = posb. by apply: val_inj => /=; apply/eqP; rewrite eqn_leq Hi andbT -ltnS. by rewrite posbinSF. congr (_ ++ _ :: _). set LS := (setI _ _); have HposcLS : posc \in LS. by rewrite /LS !inE /=; apply/andP; split. have /= -> := extract_cut (in_tuple x) HposcLS. have -> : LS :&: [set j : 'I_(size x) | j < (size u).+2] = set0. rewrite /LS -setP => i; rewrite !inE /=. apply/negP=> /andP[/andP[Hi H1] H2]. by have:= leq_ltn_trans H1 H2; rewrite ltnn. have /= -> := (extract0 (in_tuple x)); rewrite cat0s. rewrite tnth_posc; congr (_ :: extractpred (in_tuple x) (mem (pred_of_set _))). rewrite {HposcLS}/LS -setP => i; rewrite !inE. case: (ltnP (size u).+2 i) => Hi2; last by rewrite !andbF. by rewrite (ltn_trans (ltnSn _) Hi2) !andbT. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools ordcast ordtype subseq partition tableau Yamanouchi stdtab Schensted congr plactic Greene