proposition: Lemma Qbin_noboth U : U \in Qbin -> ~ ((posa \in U) && ((posc \in U))).
proof: Proof. Proof using HRabc HS HT Hposa Hposb Px. rewrite /Qbin !inE. case: (U =P S1) => [-> _ | _] /=. - by rewrite /S1 !inE Hposa /= !ltnn !andbF. case: (U =P T1) => [-> _ | _] /=. - by rewrite /T1 !inE Hposa /= posa_inTF /= ltnn. - move/andP => []; rewrite negb_or => /andP[HUS HUT] HU. move: Px => /and3P[_ /trivIsetP Htriv _]. move/(_ _ _ HU HS HUS)/disjoint_setI0/setP/(_ posa) : Htriv. by rewrite in_set0 in_setI Hposa andbT => ->. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools ordcast ordtype subseq partition tableau Yamanouchi stdtab Schensted congr plactic Greene