proposition: Theorem plact_revdual u v : u =Pl v -> revdual u =Pl revdual v.
proof: Proof. Proof using. move: v; apply: gencongr_ind; first exact: plact_refl. move=> a b1 c b2 Hu Hplact. move: Hu => /plact_trans; apply => {u}. rewrite /revdual /= !rev_cat. apply: plact_catl; apply: plact_catr. apply: rule_gencongr => /=. by move: Hplact => /plactruleP[]; rewrite !mem_cat (plact1dual, plact1idual, plact2dual, plact2idual); rewrite /revdual /= => -> ; rewrite /= ?orbT. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools partition ordtype tableau stdtab Schensted congr