proposition: Lemma sorted_leqX_tabrows t i : is_tableau t -> i < size (tabrows t) -> sorted <=%O (extract (in_tuple (to_word t)) (nth set0 (tabrows t) i)).
proof: Proof. Proof using. rewrite size_tabrows. elim: t i => [// | t0 t IHt] i. rewrite [X in X -> _]/=; move=> /and4P[_ Hrow _ Htab]. case: i IHt => [_ _ | i IHt Hi]. - by rewrite extract_tabrows_0; exact Hrow. - rewrite extract_tabrows_rec; last exact: Hi. exact: (IHt _ Htab). Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype