proposition: Theorem plact_from_dualE (u v : seq Alph^d) : u =Pl v <-> from_revdual u =Pl from_revdual v.
proof: Proof. Proof using. split; first exact: plact_from_revdual. by move /plact_revdual; rewrite !from_revdualK. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools partition ordtype tableau stdtab Schensted congr