proposition: Lemma rembig_plact1 u v : u \in (plact1 v) -> rembig u = rembig v.
proof: Proof. Proof using. move/plact1P => [a] [b] [c] [] /andP[Hab Hbc] -> -> /=. rewrite Hbc [(b < a)%O]ltNge Hab /= andbT andbF. by rewrite (le_lt_trans Hab Hbc). Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools partition ordtype tableau stdtab Schensted congr