proposition: Lemma extract_tabrows_0 : extract (in_tuple (to_word (t0 :: t))) (nth set0 (tabrows (t0 :: t)) 0) = t0.
proof: Proof. Proof using. rewrite /tabrows /= imset_comp -!imset_comp extractIE. rewrite [imset _ _](_ : _ = [set rsh_rec i | i in 'I_(size t0)]); first last. by apply/setP => i; apply/imsetP/imsetP => [] [/= x _ ->]; exists x => //=; rewrite -rcast_com /=. rewrite enumIsize_to_word filter_cat map_cat -[RHS]cat0s; congr (_ ++ _). - rewrite (eq_in_filter (a2 := pred0)); first by rewrite filter_pred0. move=> i /mapP[j Hj /= -> {i}]. by apply/negP => /imsetP[k _ /eqP]; rewrite lrshift_recF. - rewrite (eq_in_filter (a2 := predT)); first last. by move=> i /= /mapP[j _ ->{i}]; rewrite imset_f. rewrite filter_predT -map_comp. rewrite (eq_map (g := nth inh t0 \o val)); first last. + move=> i /=; rewrite (tnth_nth inh). rewrite {1 2}(to_word_cons t0 t) /= nth_cat. rewrite -{2}[size (to_word t)]addn0 ltn_add2l /=. by rewrite addnC addnK. + apply: (eq_from_nth (x0 := inh)). by rewrite size_map size_enum_ord. move=> i; rewrite size_map size_enum_ord => Hi. rewrite (nth_map (Ordinal Hi)) /=; last by rewrite size_enum_ord. by rewrite nth_enum_ord //=. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype