proposition: Lemma extract_bT : extract (in_tuple x) (T :&: [set j : 'I_(size x) | j >= posb]) = b :: extract (in_tuple x) (T :&: [set j : 'I_(size x) | j > posc]).
proof: Proof. Proof using HRabc HS HT Hposa Hposb Hposc Px. set T' := (X in extract _ X). have : posb \in T' by rewrite !inE leqnn Hposb. move /extract_cut ->. rewrite -[tnth _ _ :: _ ]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 T)) => //= Hi. case: (ltnP (size u).+2 i). + by move/ltnW/ltnW => H; rewrite H (ltnW H). + move=> Hi1; apply/negP => /andP[_ H2]. have:= TS_disjoint => /disjoint_setI0; apply/setP => Hdisj. case: (ltnP (size u).+1 i) => Hi2. * have Htmp : i = posc. by apply: val_inj => /=; apply/eqP; rewrite eqn_leq Hi2 Hi1. subst i => {Hi1 H2 Hi2}. by move/(_ posc): Hdisj; rewrite in_set0 in_setI Hi Hposc. * have Htmp : i = posa. by apply: val_inj => /=; apply/eqP; rewrite eqn_leq Hi2 H2. subst i => {Hi1 H2 Hi2}. by move/(_ posa): Hdisj; rewrite in_set0 in_setI Hi Hposa. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools ordcast ordtype subseq partition tableau Yamanouchi stdtab Schensted congr plactic Greene