proposition: Lemma size_sfiltergtn p n : is_std p -> size (sfiltergtn n p) = minn n (size p).
proof: Proof. Proof using. by move/(perm_sfiltergtn n)/perm_size ->; rewrite size_iota. 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