proposition: Lemma extract_swap_set S : S \in P -> extract (in_tuple y) (swap_set S) = extract (in_tuple x) S.
proof: Proof. Proof using HnoBoth. move=> HS; rewrite /extract /= !extractmaskE /=. rewrite (enum_cast_ord Hcast) -map_comp. rewrite Swap.enum_cut /x /y !map_cat !mask_cat //=; first last. - rewrite size_map; exact: Swap.size_cut_sizeu. - rewrite size_map; exact: Swap.size_cut_sizeu. rewrite !mem_cast. congr (mask _ u ++ _ ++ mask _ v). - apply eq_in_map => i /=. rewrite mem_filter => /andP[Hi _]. by rewrite mem_cast -{1}[i](Swap.swapL Hi) /Swap.swap_set /= mem_imset; last exact: Swap.swap_inj. - rewrite -{1}Swap.swap1 mem_imset //=; last exact: Swap.swap_inj. rewrite -{2 3}Swap.swap0 mem_imset //=; last exact: Swap.swap_inj. by move/(_ _ HS): HnoBoth; case: (posa \in S); case: (posb \in S). - apply eq_in_map => i /=. rewrite mem_filter => /andP[]; rewrite addnS addn1 => Hi _. by rewrite mem_cast -{1}[i](Swap.swapR Hi) /Swap.swap_set /= mem_imset; last exact: Swap.swap_inj. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools ordcast ordtype subseq partition tableau Yamanouchi stdtab Schensted congr plactic Greene