proposition: Lemma plact1dual u v : u \in plact1 v = (revdual u \in @plact2 _ Alph^d (revdual v)).
proof: Proof. Proof using. apply/idP/idP. - move /plact1P => [a] [b] [c] [Habc -> ->]. by rewrite /revdual /= leEdual ltEdual andbC Habc mem_seq1. - move /plact2P => [a'] [b'] [c'] [Habc']. rewrite /revdual => /(congr1 from_revdual) /= H1 /(congr1 from_revdual) /= H2. move: H1 H2; rewrite !revK => -> -> /=. by rewrite -leEdual -ltEdual andbC Habc' /= mem_seq1. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools partition ordtype tableau stdtab Schensted congr