proposition: Lemma rev_ksuppK : cancel rev_ksupp rev_ksupp_inv.
proof: Proof. Proof using. move=> S; rewrite /rev_ksupp_inv /rev_ksupp -imset_comp /=. set f := (X in imset X _). suff /eq_imset -> : f =1 id by rewrite imset_id. rewrite {}/f /rev_set => s /=. apply/setP/subset_eqP/andP. by split; apply/subsetP=> i; rewrite inE; by rewrite mem_imset; last exact rev_ord_cast_inj. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools ordcast ordtype subseq partition tableau Yamanouchi stdtab Schensted congr plactic Greene