proposition: Lemma swap_set_invol : involutive swap_set.
proof: Proof. Proof using. move=> S; apply/setP => i; rewrite -{1}[i]swap_invol. by rewrite !(mem_imset _ _ swap_inj). Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools ordcast ordtype subseq partition tableau Yamanouchi stdtab Schensted congr plactic Greene