proposition: Lemma plact1I u v : u \in plact1 v <-> v \in plact1i u.
proof: Proof. Proof using. split => [/plact1P | /plact1iP] [a] [b] [c] [H -> ->] => /=; by rewrite H mem_seq1 eq_refl. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools partition ordtype tableau stdtab Schensted congr