proposition: Theorem plact_dualE u v : u =Pl v <-> revdual u =Pl revdual v.
proof: Proof. Proof using. split; first exact: plact_revdual. rewrite -{2}[u]revdualK -{2}[v]revdualK; exact: plact_from_revdual. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools partition ordtype tableau stdtab Schensted congr