proposition: Lemma rembig_plact u v : u \in (plactrule _ v) -> rembig u = rembig v.
proof: Proof. Proof using. move/plactruleP => []. exact: rembig_plact1. exact: rembig_plact1i. exact: rembig_plact2. exact: rembig_plact2i. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools partition ordtype tableau stdtab Schensted congr