proposition: Lemma size_tabcols t : size (tabcols t) = size (head [::] t).
proof: Proof. Proof using. by rewrite /tabcols /= size_map size_shcols; case t. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype