proposition: Lemma ksupp_Q : Q \is a k.-supp[R, in_tuple y].
proof: Proof. Proof using HnoBoth Px. move: Px => /and3P[HszP HtrivP /forallP /= HallP]. apply/and3P; split. - by rewrite card_imset; last exact swap_set_inj. - rewrite /Q /swap_set imset_comp. apply: imset_trivIset; first exact: cast_ord_inj. apply: imset_trivIset; first exact: Swap.swap_inj. exact HtrivP. - apply/forallP => S2; apply/implyP => /imsetP[S HS ->{S2}]. rewrite (extract_swap_set HS). by move/(_ S): HallP; rewrite HS. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools ordcast ordtype subseq partition tableau Yamanouchi stdtab Schensted congr plactic Greene