proposition: Lemma sorted_gt_tabcols t i : is_tableau t -> i < size (tabcols t) -> sorted >%O (extract (in_tuple (to_word t)) (nth set0 (tabcols t) i)).
proof: Proof. Proof using. elim: t => [// | t0 t IHt]. rewrite [X in X -> _]/=; move=> /and4P[_ _ /dominateP[Hsz Hdom] Htab]. rewrite size_tabcols_cons => Hi; rewrite (extract_tabcols_rec _ Hi). case (ltnP i (size (head [::] t))) => Hit. - have:= Hit; rewrite -size_tabcols; move/(IHt Htab) => {IHt}. move Hrec : (extract _ _) => ext. case: ext Hrec => [//= | a0 ext] Hext. rewrite rcons_cons /= rcons_path => -> /=. suff -> : last a0 ext = nth inh (head [::] t) i by exact: Hdom. rewrite -[last a0 ext]/(last inh (a0 :: ext)) -Hext {a0 ext Hext}. case: t Hsz Htab Hit {Hdom} => [// | t1 t] Hsz Htab Hit. by rewrite (extract_tabcols_rec _ Hit) last_rcons. - rewrite nth_default; last by rewrite size_tabcols. by rewrite extract0. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype