proposition: Lemma extract_cS : extract (in_tuple x) (S :&: [set j : 'I_(size x) | j >= posc]) = c :: extract (in_tuple x) (S :&: [set j : 'I_(size x) | j > posc]).
proof: Proof. Proof using Hposc. set S' := (X in extract _ X). have : posc \in S' by rewrite !inE leqnn Hposc. move /extract_cut ->; rewrite -cat1s -[RHS]cat1s -[RHS]cat0s. congr (_ ++ _ ++ (extract (in_tuple x) _)). - set s := (X in extract _ X); suff -> : s = set0 by rewrite extract0. rewrite {}/s -setP => i; rewrite !inE -andbA. apply/negP => /and3P[_ H1 H2]. by have:= leq_trans H2 H1; rewrite ltnn. - by rewrite (tnth_nth a) /x /=; elim: u. - apply/setP => i; rewrite !inE. case: (boolP (i \in S)) => //= _. case: (ltnP (size u).+2 i); last by rewrite andbF. by move/ltnW ->. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools ordcast ordtype subseq partition tableau Yamanouchi stdtab Schensted congr plactic Greene