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