proposition: Lemma rembig_plact1i u v : u \in (plact1i v) -> rembig u = rembig v.
proof: Proof. Proof using. by rewrite -plact1I => /rembig_plact1 ->. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools partition ordtype tableau stdtab Schensted congr