proposition: Lemma rev_set_inj : injective rev_set.
proof: Proof. Proof using. by move=> i j /=; rewrite /rev_set; apply: imset_inj; exact rev_ord_cast_inj. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools ordcast ordtype subseq partition tableau Yamanouchi stdtab Schensted congr plactic Greene