proposition: Lemma ksupp_bin : Qbin \is a k.-supp[R, in_tuple x].
proof: Proof. Proof using HRabc HS HT Hposa Hposb Hposc Px. move: Px => /and3P[HszP HtrivP /forallP HallP]. rewrite /Qbin; apply/and3P; split. - move: HszP. rewrite -setDDl (cardsD1 S P) (cardsD1 T (P :\ S)) HS /=. have -> /= : T \in P :\ S by rewrite !inE TSneq HT. apply: leq_trans; rewrite addnA add1n. apply: (leq_trans (leq_card_setU _ _)); rewrite leq_add2r. by apply: (leq_trans (leq_card_setU _ _)); rewrite !cards1. - exact: trivIset_Qbin. - apply/forallP => U; apply/implyP; rewrite !inE => /orP[]; first move => /orP[]. + by move/eqP => H; subst U; exact: extract_S1. + by move/eqP => H; subst U; exact: extract_T1. + by rewrite negb_or => /andP[_ HU]; have := HallP U; rewrite HU /=. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools ordcast ordtype subseq partition tableau Yamanouchi stdtab Schensted congr plactic Greene