proposition: Lemma ksupp_inj_invseq k : ksupp_inj <=%O <=%O k s t.
proof: Proof. Proof using Hinv s t. rewrite /ksupp_inj /ksupp => ks /and3P[Hsz Htriv /forallP Hall]. exists [set val2pos @: (p : {set 'I_(size s)}) | p in ks]. apply/and4P; split. - by rewrite /=; apply/eqP; apply: size_cover_inj; exact: val2pos_inj. - exact: (leq_trans (leq_imset_card _ _) Hsz). - exact: (imset_trivIset val2pos_inj). - apply/forallP => ptmp; apply/implyP => /imsetP[p Hp ->{ptmp}]. move/(_ p): Hall; rewrite Hp /= /extractpred. move/val2pos_enum ->; rewrite -map_comp /=. rewrite (eq_map (g := nat_of_ord)); first last. move=> i /=; rewrite (tnth_nth (size s)) /=. by have:= Hinvst => /linvseqP ->. set l := map _ _; have : subseq l [seq val x | x <- enum 'I_(size s)]. apply: map_subseq; rewrite /enum_mem. rewrite [X in subseq _ X](eq_filter (a2 := xpredT)) //. by rewrite filter_predT; exact: filter_subseq. move/subseq_sorted; apply; first by move=> a b c H1 H2; exact: le_trans H1 H2. by rewrite val_enum_ord; exact: iota_sorted. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordcast partition Yamanouchi ordtype std tableau stdtab sorted Schensted congr plactic Greene Greene_inv