proposition: Lemma size_tabcols_cons : size (tabcols (t0 :: t)) = size t0.
proof: Proof. Proof using. by rewrite tabcols_cons /= size_map size_enum_ord. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype