proposition: Lemma swap_invol : involutive swap.
proof: Proof. Proof using. rewrite /swap => i. case: (i =P pos0) => [-> | /eqP H0]; first by rewrite eq_sym pos01F eq_refl. case: (i =P pos1) => [-> | /eqP H1]; first by rewrite eq_refl. by rewrite (negbTE H0) (negbTE H1). Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools ordcast ordtype subseq partition tableau Yamanouchi stdtab Schensted congr plactic Greene