proposition: Lemma Qbnotin_noboth T : T \in Qbnotin -> ~ ((posa \in T) && (posc \in T)).
proof: Proof. Proof using HS HbNin. rewrite /Qbnotin => /imsetP[U HU ->{T}]. case: (U =P S) => Heq. - subst U; rewrite -Swap.swap0 /swap_set /=. rewrite mem_imset; last apply: Swap.swap_inj. by rewrite posbinSF. - rewrite -Swap.swap0 /swap_set /=. rewrite mem_imset; last apply: Swap.swap_inj. move/andP => [Hb _]; move: HbNin. by rewrite (_ : _ \in _); last by rewrite /cover; apply/bigcupP; exists U. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools ordcast ordtype subseq partition tableau Yamanouchi stdtab Schensted congr plactic Greene