proposition: Lemma Hcast : size x = size y.
proof: Proof. Proof using a b u v. by rewrite !size_cat. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools ordcast ordtype subseq partition tableau Yamanouchi stdtab Schensted congr plactic Greene