proposition: Lemma sorted_center u v w : sorted >%O (u ++ v ++ w) -> sorted >%O v.
proof: Proof. Proof using. rewrite /sorted; case: u => [| u0 u] /=. case: v => [// | v0 v] /=. by rewrite cat_path => /andP[]. case: v => [// | v0 v] /=. rewrite !cat_path => /andP[/= _ /andP[_]]. by rewrite cat_path => /andP[]. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools partition ordtype tableau stdtab Schensted congr