proposition: Lemma perm_sfilterleq p n : is_std p -> perm_eq (sfilterleq n p) (iota 0 ((size p) - n)).
proof: Proof. Proof using . move=> Hstd; apply: uniq_perm. - rewrite map_inj_in_uniq. + by apply: filter_uniq; exact: std_uniq. + move=> i j; rewrite !mem_filter => /andP[Hi _] /andP[Hj _] H. by rewrite -(subnK Hi) H (subnK Hj). - exact: iota_uniq. - move=> i; rewrite mem_sfilterleqK. rewrite (perm_mem Hstd). rewrite !mem_iota /= !add0n. by rewrite ltn_subRL addnC. 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