proposition: Lemma extract_Sa : extract (in_tuple x) (S :&: [set j : 'I_(size x) | j <= posa]) = rcons (extract (in_tuple x) (S :&: [set j : 'I_(size x) | j < posa])) a.
proof: Proof. Proof using Hposa. set S' := (X in extract _ X). have : posa \in S' by rewrite /S' !inE leqnn Hposa. rewrite /S'; move /extract_cut ->. rewrite -cats1 -[X in _ = _ ++ X]cats0 -[tnth _ _ :: _]cat1s. congr ((extract (in_tuple x) _) ++ _ ++ _). - apply/setP => i; rewrite !inE. case: (boolP (i \in S)) => //= _. case: (ltnP i (size u).+1); last by rewrite andbF. by move/ltnW ->. - by rewrite (tnth_nth a) /x /=; elim: u. - 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. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools ordcast ordtype subseq partition tableau Yamanouchi stdtab Schensted congr plactic Greene