proposition: Lemma perm_sfiltergtn p n : is_std p -> perm_eq (sfiltergtn n p) (iota 0 (minn n (size p))).
proof: Proof. Proof using . move=> Hstd; apply: uniq_perm. - by apply: filter_uniq; exact: std_uniq. - exact: iota_uniq. - move=> i; rewrite mem_filter mem_iota /= add0n leq_min. congr (_ && _). rewrite (perm_mem Hstd). by rewrite mem_iota /= add0n. 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