proposition: Theorem exists_Q_noboth : exists Q : {set {set 'I_(size x)}}, [/\ Q \is a k.-supp[R, in_tuple x], #|cover Q| = #|cover P| & forall S, S \in Q -> ~ ((posa \in S) && ((posc \in S)))].
proof: Proof. Proof using HRabc HS Hposa Hposc Px. case (boolP (posb \in (cover P))) => [/bigcupP[T HT HbT] | Hcov]. - exists (Qbin T); split => [||S0]. + exact: ksupp_bin. + by rewrite cover_bin. + exact: Qbin_noboth. - exists Qbnotin; split => [||S0]. + exact: ksupp_bnotin. + by rewrite (eqP (size_cover_bnotin)). + exact: Qbnotin_noboth. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools ordcast ordtype subseq partition tableau Yamanouchi stdtab Schensted congr plactic Greene