proposition: Lemma plact1iP u v : reflect (exists a b c, [/\ (a <= b < c)%O, v = [:: a; c; b] & u = [:: c; a; b] ] ) (v \in plact1i u).
proof: Proof. Proof using. apply: (iffP idP). - case: u => [//|u0[//|u1[//|u2[]//=]]]; case H : ((u1 <= u2 < u0)%O). + by rewrite mem_seq1 => /eqP ->; exists u1, u2, u0. + 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