proposition: Lemma swap_inj : injective swap.
proof: Proof. Proof using. exact (can_inj swap_invol). Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools ordcast ordtype subseq partition tableau Yamanouchi stdtab Schensted congr plactic Greene