proposition: Lemma size_shcols_cons s0 sh : size (shcols (s0 :: sh)) = s0.
proof: Proof. Proof using. by rewrite /= size_map size_enum_ord. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype