proposition: Lemma extract_Tb : extract (in_tuple x) (T :&: [set j : 'I_(size x) | j <= posb]) = rcons (extract (in_tuple x) (T :&: [set j : 'I_(size x) | j < posb])) b.
proof: Proof. Proof using Hposb. set T' := (X in extract _ X). have : posb \in T' by rewrite /T' !inE leqnn Hposb. move /extract_cut ->; rewrite -cats1 -[[:: b]]cats0 -[tnth _ _ :: _]cat1s. congr ((extract (in_tuple x) _) ++ _ ++ _). - apply/setP => i; rewrite !inE. case: (boolP (i \in T)) => //= _. case: (ltnP i (size u)); 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