proposition: Lemma std_plact1 (u v1 w v2 : seq Alph) : v2 \in plact1 v1 -> std (u ++ v1 ++ w) =Pl std (u ++ v2 ++ w).
proof: Proof. Proof using. move/plact1P => [a] [b] [c] [Habc -> ->]. have:= std_cutabc u w a c b => [] [U] [V] [A] [C] [B] [Hsz Hstd]. have Hac : (a < c)%O by move: Habc => /andP[]; apply: le_lt_trans. rewrite Hstd (std_transp Hac Hsz Hstd) -[[:: C; A] ++ B :: V]/([:: C; A; B] ++ V). apply: plact_catr; apply: plact_catl. apply: rule_gencongr => /=. suff -> : (A <= B < C)%O by rewrite inE eq_refl. have:= eq_inv_std (u ++ [:: a; c; b] ++ w). rewrite Hstd {Hstd} => /eq_invP[Hsize Hinv]. have:= Hinv (size u) (size u).+2. set Hyp := (X in (X -> _ ) -> _) => Hinvab. have {Hyp} /Hinvab : Hyp. rewrite /Hyp (leq_trans (leqnSn _) (leqnSn _)) /= size_cat /=. by rewrite -2!addSnnS -{1}[(size u).+2]addn0 ltn_add2l. rewrite {3 4}Hsz !nth_sizeu !nth_sizeu2 => <-. move/(_ (size u).+1 (size u).+2): Hinv. set Hyp := (X in (X -> _ ) -> _) => Hinvbc. have {Hyp} /Hinvbc : Hyp. rewrite /Hyp (ltn_trans (ltnSn _) (ltnSn _)) /= size_cat /=. by rewrite -2!addSnnS -{1}[(size u).+2]addn0 ltn_add2l. rewrite {3 4}Hsz !nth_sizeu1 !nth_sizeu2 ltNge => <-. by rewrite -ltNge. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordcast partition Yamanouchi ordtype std tableau stdtab sorted Schensted congr plactic Greene Greene_inv