proposition: Lemma invstd_catgtn u v : invstd (std u) = sfiltergtn (size u) (invstd (std (u ++ v))).
proof: Proof. Proof using . have Hsftstd : is_std (sfiltergtn (size u) (invstd (std (u ++ v)))). apply: (@sfiltergtn_is_std (invstd (std (u ++ v))) (size u)). by apply: invstd_is_std; exact: std_is_std. suff Heqinv : std u = invstd (sfiltergtn (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_sfiltergtn_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_sfiltergtn_cat). rewrite index_leq_filter //= -/(invstd (std (u++v))). have Hucat : size u <= size (std (u ++ v)). by rewrite size_std size_cat; apply: leq_addr. do 2 (rewrite (index_invstd (std_is_std (u ++ v))); last by apply: (@leq_trans (size u)); last exact Hucat). have /eq_invP := eq_inv_std (u ++ v) => [] [_ Hinv]. have Hijsz : i <= j < size (u ++ v). rewrite Hij /=; apply: (leq_trans Hj); rewrite size_cat; exact: leq_addr. rewrite -leEnat -(Hinv i j Hijsz). by rewrite !nth_cat Hi Hj. 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