proposition: Lemma ksupp_bnotin : Qbnotin \is a k.-supp[R, in_tuple x].
proof: Proof. Proof using HRabc HS HbNin Hposa Hposc Px. move: Px => /and3P[HszP HtrivP /forallP HallP]. apply/and3P; split. - by rewrite card_imset; last apply: Swap.swap_set_inj. - rewrite /Qbnotin /swap_set. apply: imset_trivIset; first exact: Swap.swap_inj. exact HtrivP. - apply/forallP => T2; apply/implyP => /imsetP[T HT ->{T2}]. case/altP: (T =P S) => Heq. + subst T; exact: extract_swap_set_S. + apply: extract_swap_set. * move: Heq; apply: contra => /eqP H; apply/eqP; exact: Swap.swap_set_inj. * by rewrite /Qbnotin mem_imset; last exact: Swap.swap_set_inj. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools ordcast ordtype subseq partition tableau Yamanouchi stdtab Schensted congr plactic Greene