proposition: Lemma size_to_word_cons : size (to_word t) + size t0 = size (to_word (t0 :: t)).
proof: Proof. Proof using. by rewrite !size_to_word /size_tab /= addnC. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype