proposition: Lemma extract_tabcols_rec i : i < size t0 -> extract (in_tuple (to_word (t0 :: t))) (nth set0 (tabcols (t0 :: t)) i) = rcons (extract (in_tuple (to_word t)) (nth set0 (tabcols t) i)) (nth inh t0 i).
proof: Proof. Proof using. move => Hi; rewrite /= !extractmaskE tabcols_cons enumIsize_to_word /=. rewrite (nth_map (Ordinal Hi)); last by rewrite size_enum_ord. rewrite nth_enum_ord //= [X in mask _ X]to_word_cons. rewrite nth_ord_ltn map_cat mask_cat; last by rewrite 2!size_map size_enum_ord. rewrite -map_comp. set fr := (X in rcons (mask (map X _) _)). rewrite (eq_map (g := fr)); first last. move=> j /=; rewrite inE in_set1 lrshift_recF /=. by rewrite (mem_imset _ _ lshift_recP). rewrite -map_comp. set f2 := (X in _ ++ mask (map X _) _). have {f2} /eq_map -> : f2 =1 mem ([set (Ordinal Hi)]). move=> j; rewrite /f2 /= !inE. rewrite [X in _ || X](_ : _ = false); first last. by apply/imsetP => [[k _] /eqP]; rewrite eq_sym lrshift_recF. rewrite orbF. by apply/idP/idP => [/eqP/rshift_recP ->|/eqP ->]. have := extract1 (in_tuple t0) (Ordinal Hi). rewrite /extract /= extractmaskE /= => ->. by rewrite cats1 (tnth_nth inh) /=. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype