proposition: Theorem plactic_RS u v : u =Pl v <-> RS u == RS v.
proof: Proof. Proof using. split; last exact: Sch_plact. move Hu : (size u) => n Hpl. have:= perm_size (plact_homog Hpl) => /esym; rewrite Hu. elim: n u v Hpl Hu => [| n IHn] u v. by move=> _ /eqP/nilP -> /eqP/nilP ->; rewrite /RS. move=> Hpl Hu Hv. have:= size_rembig u; rewrite Hu /= => Hszu. have:= size_rembig v; rewrite Hv /= => Hszv. move/(_ _ _ (rembig_plactcongr Hpl) Hszu Hszv): IHn => /eqP {Hszu Hszv}. case: u Hu Hpl => // u0 u' _. case: v Hv => // v0 v' _ => Hpl Hplrem. have [iu Hiu] := rembig_RS u0 u'. have [iv] := rembig_RS v0 v'; rewrite -{}Hplrem => Hiv. rewrite -(maxL_perm (plact_homog Hpl)) in Hiv. have:= plactic_shapeRS Hpl. by rewrite {}Hiu {}Hiv !shape_append_nth => /incr_nth_inj<-. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools ordcast ordtype subseq partition tableau Yamanouchi stdtab Schensted congr plactic Greene