proposition: Lemma plact2iP u v : reflect (exists a b c, [/\ (a < b <= c)%O, v = [:: b; a; c] & u = [:: b; c; a] ] ) (v \in plact2i u).
proof: Proof. Proof using. apply: (iffP idP). - case: u => [//|u0[//|u1[//|u2[]//=]]]; case H : ((u2 < u0 <= u1)%O). + by rewrite mem_seq1 => /eqP ->; exists u2, u0, u1. + by rewrite in_nil. - by move=> [a] [b] [c] [H -> ->]; rewrite /= H mem_seq1 eq_refl. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools partition ordtype tableau stdtab Schensted congr