proposition: Lemma size_sfilterleq_cat u v : size (sfilterleq (size u) (invstd (std (u ++ v)))) = size v.
proof: Proof. Proof using . rewrite (size_sfilterleq _ (invstd_is_std _)); last exact: std_is_std. by rewrite size_invstd size_std size_cat addKn. 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