proposition: Lemma std_plact2 (u v1 w v2 : seq Alph) : v2 \in plact2 v1 -> std (u ++ v1 ++ w) =Pl std (u ++ v2 ++ w).
proof: Proof. Proof using. have reorg3 (T : eqType) (U W : seq T) b a c : U ++ [:: b; a; c] ++ W = (U ++ [:: b]) ++ [:: a; c] ++ W by rewrite -catA. move/plact2P => [a] [b] [c] [Habc -> ->]. have:= std_cutabc u w b a c => [] [U] [W] [B] [A] [C] [Hsz]. have Hac : (a < c)%O by move: Habc => /andP[]; apply: lt_le_trans. rewrite !reorg3. have Hsz1 : size (u ++ [:: b]) = size (U ++ [:: B]) by rewrite !size_cat Hsz. move=> Hstd; rewrite Hstd (std_transp Hac Hsz1 Hstd). rewrite -!reorg3. apply: plact_catr; apply: plact_catl. apply: rule_gencongr => /=. suff -> : (A < B <= C)%O by rewrite !mem_cat inE eq_refl /= !orbT. rewrite -!reorg3 in Hstd. have:= eq_inv_std (u ++ [:: b; a; c] ++ w). rewrite {}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) (size u).+1): Hinv. set Hyp := (X in (X -> _ ) -> _) => Hinvbc. have {Hyp}/Hinvbc : Hyp. rewrite /Hyp (leqnSn _) /= size_cat /=. by rewrite -addSnnS -{1}[(size u).+1]addn0 ltn_add2l. rewrite {3 4}Hsz !nth_sizeu !nth_sizeu1 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