proposition: Lemma invstd_catleq u v : invstd (std v) = sfilterleq (size u) (invstd (std (u ++ v))).
proof: Proof. Proof using . have Hsftstd : is_std (sfilterleq (size u) (invstd (std (u ++ v)))). apply: (@sfilterleq_is_std (invstd (std (u ++ v))) (size u)). by apply: invstd_is_std; exact: std_is_std. suff Heqinv : std v = invstd (sfilterleq (size u) (invstd (std (u ++ v)))). by rewrite Heqinv invstdK. apply/eqP/stdP; apply: StdSpec; first exact: invstd_is_std. move=> {Hsftstd}. apply/eq_invP; split; first by rewrite size_invstd size_sfilterleq_cat. move=> i j /andP[Hij Hj]. have Hi := leq_ltn_trans Hij Hj. rewrite leEnat /=. do 2 (rewrite nth_mkseq; last by rewrite size_sfilterleq_cat). rewrite !index_sfilterleq index_leq_filter; try apply: leq_addl. do 2 (rewrite (index_invstd (std_is_std (u ++ v))); last by rewrite size_std size_cat addnC ltn_add2l). have /eq_invP := eq_inv_std (u ++ v) => [] [_ Hinv]. have Hijsz : i + size u <= j + size u < size (u ++ v). rewrite size_cat [size u + _]addnC. rewrite leq_add2r ltn_add2r. by rewrite Hij Hj. rewrite -leEnat -(Hinv _ _ Hijsz) {Hijsz}. rewrite !nth_cat. have H x : (x + size u < size u) = false. by apply: negbTE; rewrite -leqNgt; apply: leq_addl. by rewrite !H !addnK. 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