proposition: Lemma inPQE T : T != swap_set S -> T \in Qbnotin -> T \in P.
proof: Proof. Proof using HS HbNin Hposa Px. rewrite /Qbnotin => Hneq /imsetP[TP HTP Hswap]; subst T. have {}Hneq : TP != S by move: Hneq; apply: contra => /eqP ->. suff -> : swap_set TP = TP by []. rewrite /swap_set /= -setP /Swap.swap => i. rewrite (eq_in_imset (g := id)); first by rewrite imset_id. move=> {}i /= Hi. have -> : (i == posb) = false. apply/negP => /eqP //= Hib; subst i. have Hcov : posb \in cover P by rewrite /cover; apply/bigcupP; exists TP. by move: HbNin; rewrite Hcov. suff -> : (i == posa) = false by []. apply/negP => /eqP //= Hib; subst i. move: Px => /and3P[_ /trivIsetP Htriv _]. move/(_ _ _ HTP HS Hneq) : Htriv => /disjoint_setI0. apply/setP => /(_ posa); rewrite in_set0 in_setI Hi. by rewrite Hposa. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools ordcast ordtype subseq partition tableau Yamanouchi stdtab Schensted congr plactic Greene