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