proposition: Theorem invstd_cat_in_shsh u v : invstd (std (u ++ v)) \in shsh (invstd (std u)) (invstd (std v)).
proof: Proof. Proof using . rewrite mem_shsh; last by apply: invstd_is_std; apply: std_is_std. rewrite {2}(invstd_catgtn u v) size_invstd size_std (invstd_catleq u v). by rewrite !eq_refl. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype finfun fintype choice) mathcomp(order seq tuple finset perm binomial bigop) tools vectNK subseq partition Yamanouchi ordtype std tableau stdtab Schensted plactic Greene_inv stdplact