proposition: Lemma extract_swap_setSE : extract (in_tuple x) (swap_set S) = (extract (in_tuple x) (S :&: [set j : 'I_(size x) | j < size u])) ++ b :: c :: extract (in_tuple x) (S :&: [set j : 'I_(size x) | (size u).+2 < j]).
proof: Proof. Proof using HS HbNin Hposa Hposc. have /extract_cut -> /= : posb \in (swap_set S). by rewrite /swap_set /= -Swap.swap1; apply: imset_f. rewrite (_ : setI [set Swap.swap x | x in S] _ = S :&: [set j : 'I_(size x) | j < size u]); first last. rewrite -!setIdE -setP => /= i; rewrite !inE. case: (ltnP i (size u)) => Hi; last by rewrite !andbF. rewrite !andbT -{1}(Swap.swapL Hi) mem_imset //=. exact: Swap.swap_inj. congr (_ ++ _ :: _); first by rewrite (tnth_nth b) /= nth_cat ltnn subnn. set LS := (setI (imset _ _) _). have HposcLS : posc \in LS. rewrite /LS !inE /=; apply/andP; split; last by []. rewrite -(Swap.swapR (i := posc)) //. rewrite mem_imset //=; exact: Swap.swap_inj. 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 /=. case: (ltnP (size u) i) => Hi; last by rewrite andbF. case: (ltnP i (size u).+2) => Hi2; last by rewrite andbF. rewrite (_ : i = posa); first last. by apply: val_inj => /=; apply/eqP; rewrite eqn_leq Hi andbT -ltnS. rewrite -Swap.swap0 mem_imset //=; last exact: Swap.swap_inj. by rewrite posbinSF. 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) => Hi; last by rewrite !andbF. rewrite -{1}(Swap.swapR (ltnW Hi)) mem_imset //=; last exact: Swap.swap_inj. rewrite andbT; congr (_ && _). exact: (ltn_trans (ltn_trans (ltnSn _) (ltnSn _)) Hi). Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools ordcast ordtype subseq partition tableau Yamanouchi stdtab Schensted congr plactic Greene