proposition: Lemma sfiltergtn_invstd w n : n <= size w -> sfiltergtn n (invstd (std w)) = invstd (std (take n w)).
proof: Proof. move=> Hn. have Hsftstd : is_std (sfiltergtn n (invstd (std w))). apply: (@sfiltergtn_is_std (invstd (std w)) n). by apply: invstd_is_std; exact: std_is_std. suff Heqinv : invstd (sfiltergtn n (invstd (std w))) = std (take 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_takel // size_invstd size_sfiltergtn //. by rewrite size_invstd size_std (minn_idPl Hn). move=> i j /andP[Hij]; rewrite size_takel // => Hj. have Hi := leq_ltn_trans Hij Hj. rewrite leEnat /=. do 2 (rewrite nth_mkseq; last rewrite size_sfiltergtn //; last by rewrite size_invstd size_std (minn_idPl Hn)). rewrite index_leq_filter // !nth_take //. rewrite (index_invstd (std_is_std w)); first last. by apply (leq_trans Hi); rewrite size_std. rewrite (index_invstd (std_is_std w)); first last. by apply (leq_trans Hj); rewrite size_std. have /eq_invP := (eq_inv_std w) => [] [_]; apply. by rewrite Hij (leq_trans Hj Hn). 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