proposition: Lemma swapL (i : 'I_(size x)) : i < size u -> swap i = i.
proof: Proof. Proof using. move=> Hi. by rewrite /swap /eq_op /= (ltn_eqF Hi) (ltn_eqF (ltn_trans (Hi) (ltnSn _))). Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools ordcast ordtype subseq partition tableau Yamanouchi stdtab Schensted congr plactic Greene