proposition: Lemma u1lt : (size u).+1 < size x.
proof: Proof. Proof using l0 l1 v. by rewrite /= size_cat /= addnS ltnS -{1}[size u]addn0 ltn_add2l. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools ordcast ordtype subseq partition tableau Yamanouchi stdtab Schensted congr plactic Greene