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