proposition: Lemma size_sfiltergtn_cat u v : size (sfiltergtn (size u) (invstd (std (u ++ v)))) = size u.
proof: Proof. Proof using . rewrite (size_sfiltergtn _ (invstd_is_std _)); last exact: std_is_std. rewrite size_invstd size_std size_cat. by have /minn_idPl -> : size u <= size u + size v by apply: leq_addr. 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