proposition: Lemma sfilterleq_invstd w n : n <= size w -> sfilterleq n (invstd (std w)) = invstd (std (drop n w)).
proof: Proof. move=> Hn. have Hsftstd : is_std (sfilterleq n (invstd (std w))). apply: (@sfilterleq_is_std (invstd (std w)) n). by apply: invstd_is_std; exact: std_is_std. suff Heqinv : invstd (sfilterleq n (invstd (std w))) = std (drop n w). by rewrite -Heqinv invstdK. apply/esym/eqP/stdP; apply: StdSpec; first exact: invstd_is_std. have Hstdiw : is_std (invstd (std w)). by apply: invstd_is_std; exact: std_is_std. apply/eq_invP; split. rewrite size_drop size_invstd size_sfilterleq //. by rewrite size_invstd size_std. move=> i j /andP[Hij]; rewrite size_drop => Hj. rewrite leEnat /=. have Hi := leq_ltn_trans Hij Hj. do 2 (rewrite nth_mkseq; last by rewrite size_sfilterleq // size_invstd size_std). rewrite !index_sfilterleq !nth_drop. rewrite index_leq_filter ?leq_addl //. do 2 (rewrite (index_invstd (std_is_std w)); last by rewrite size_std addnC -ltn_subRL). have /eq_invP := (eq_inv_std w) => [] [_]. rewrite ![_ + n]addnC; apply. by rewrite leq_add2l Hij /= -ltn_subRL. 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