proposition: Lemma size_shcols sh : size (shcols sh) = head 0 sh.
proof: Proof. Proof using. by case sh => [// | s0 s]; apply: size_shcols_cons. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype