proposition: Lemma extract_cut (N : nat) (wt : N.-tuple Alph) (i : 'I_N) (S : {set 'I_N}) : i \in S -> extract wt S = extract wt (S :&: [set j : 'I_N | j < i]) ++ (tnth wt i) :: extract wt (S :&: [set j : 'I_N | j > i]).
proof: Proof. Proof using. move=> Hi; rewrite /extract /= extractIE. rewrite -{1}[enum _](cat_take_drop i.+1) drop_enumI take_enumI !filter_cat map_cat. rewrite -{1}[enum _](cat_take_drop i) drop_enumI take_enumI !filter_cat map_cat. rewrite -cat1s catA -!filter_predI. congr (((map (tnth wt) _) ++ _) ++ (map (tnth wt) _)). - apply eq_filter => j /=; rewrite !inE !andbT. congr ((j \in S) && _); case (ltnP j i) => H; last by rewrite andbF. by rewrite (ltn_trans H (ltnSn i)). - rewrite [X in map _ X](_ : _ = [:: i]) //. rewrite (eq_filter (a2 := xpred1 i)); first last. move=> j /=; rewrite ltnS -eqn_leq inE andbT. case: (j =P i) => [-> | H]; first by rewrite eq_refl Hi. suff /negbTE -> : (val j != val i) by rewrite andbF. by apply/contra_notN: H => /eqP/val_inj ->. apply: filter_pred1_uniq; first by rewrite -enumT; apply: enum_uniq. by rewrite -enumT mem_enum inE. - by apply eq_filter => j /=; rewrite !inE !andbT. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools ordcast ordtype subseq partition tableau Yamanouchi stdtab Schensted congr plactic Greene