proposition: Lemma rev_ksuppKV : cancel rev_ksupp_inv rev_ksupp.
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; split; apply/subsetP=> i. - by move=> /imsetP[t]; rewrite inE => Ht Hi; subst i. - move=> Hi; apply/imsetP. exists (rev_ord ((cast_ord (esym (size_revdual w))) i)). + by rewrite /rev_ord_cast inE /= rev_ordK cast_ordKV. + by rewrite /rev_ord_cast /= rev_ordK cast_ordKV. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools ordcast ordtype subseq partition tableau Yamanouchi stdtab Schensted congr plactic Greene