proposition: Lemma plactruleP u v : reflect ([\/ v \in plact1 u, v \in plact1i u, v \in plact2 u | v \in plact2i u ]) (v \in plactrule u).
proof: Proof. Proof using. apply: (iffP idP). - by rewrite /plactrule /= !mem_cat => /or4P. - by rewrite /plactrule /= !mem_cat => H; apply/or4P. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools partition ordtype tableau stdtab Schensted congr