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