proposition: Lemma size_shrows sh : size (shrows sh) = size sh.
proof: Proof. Proof using. by elim: sh => [// | sh0 sh] /=; rewrite !size_map => ->. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype