proposition: Lemma sfilterleq_is_std p n : is_std p -> is_std (sfilterleq n p).
proof: Proof. Proof using . move=> Hstd; rewrite /is_std (size_sfilterleq _ Hstd). exact: perm_sfilterleq. 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