proposition: Theorem std_plact u v : u =Pl v -> std u =Pl std 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). move: Hplact {H} => /plactruleP[]. - exact: std_plact1. - rewrite -plact1I => /std_plact1-/(_ a c)/plact_ltrans <-; exact: plact_refl. - exact: std_plact2. - rewrite -plact2I => /std_plact2-/(_ a c)/plact_ltrans <-; exact: plact_refl. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordcast partition Yamanouchi ordtype std tableau stdtab sorted Schensted congr plactic Greene Greene_inv