proposition: Theorem rembig_plactcongr u v : u =Pl v -> (rembig u) =Pl (rembig v).
proof: Proof. Proof using. move: v; apply: gencongr_ind; first exact: plact_refl. move=> a b1 c b2 => H Hplact. rewrite (plact_ltrans H). have:= plactrule_homog b1 => {u H} /allP/(_ _ Hplact) Heq. have:= Heq; rewrite -(perm_cat2r c) => Heqc. have:= rembig_eq_permR _ Heqc => /(_ a) [] [-> ->]. - by apply: plact_is_congr; exact: rule_gencongr. - apply: plact_catr. have:= rembig_eq_permL _ Heq => /(_ c) [] [-> ->]. + by apply: plact_catl; rewrite (rembig_plact Hplact); exact: plact_refl. + by apply: plact_catl; exact: rule_gencongr. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools partition ordtype tableau stdtab Schensted congr