proposition: Lemma swap_set_inj : injective swap_set.
proof: Proof. Proof using. rewrite /swap_set. apply: inj_comp; last exact: Swap.swap_set_inj. apply: imset_inj; exact: cast_ord_inj. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools ordcast ordtype subseq partition tableau Yamanouchi stdtab Schensted congr plactic Greene