proposition: Lemma ksupp_inj_stdI u k : ksupp_inj <=%O <=%O k (std u) u.
proof: Proof. Proof using. rewrite /ksupp_inj /ksupp => ks /and3P[Hsz Htriv /forallP Hall]. exists (cast_set (size_std u) @: ks). apply/and4P; split. - rewrite cover_cast /cast_set /=. by rewrite card_imset; last exact: cast_ord_inj. - apply: (@leq_trans #|ks|); last exact: Hsz. exact: leq_imset_card. - apply: imset_trivIset; last exact: Htriv. exact: cast_ord_inj. - apply/forallP => Sstd; apply/implyP => /imsetP[S HS ->{Sstd}]. move/(_ S): Hall; rewrite HS /=. rewrite sorted_std_extract; congr (path.sorted _ ). rewrite /extractpred; congr (map _ _). apply: eq_enum => i. rewrite inE /cast_set /= -imset_comp. rewrite (eq_imset (g := id)); first last. by move=> j; rewrite /= (cast_ordK (size_std u)). by rewrite imset_id inE. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordcast partition Yamanouchi ordtype std tableau stdtab sorted Schensted congr plactic Greene Greene_inv