proposition: Lemma size_tabrows t : size (tabrows t) = size t.
proof: Proof. Proof using. by rewrite /tabrows /= size_map size_shrows size_map. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype