proposition: Lemma plact1idual u v : u \in plact1i v = (revdual u \in plact2i (revdual v)).
proof: Proof. Proof using. by apply/idP/idP; rewrite -plact1I -plact2I plact1dual. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools partition ordtype tableau stdtab Schensted congr