proposition: Lemma plactrule_sym u v : v \in (plactrule u) -> u \in (plactrule v).
proof: Proof. Proof using. move/plactruleP => [] /=; rewrite !mem_cat. - by rewrite plact1I => ->; rewrite !orbT. - by rewrite -plact1I => ->. - by rewrite plact2I => ->; rewrite !orbT. - by rewrite -plact2I => ->; rewrite !orbT. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools partition ordtype tableau stdtab Schensted congr