proposition: Lemma extract_tabrows_rec i : i < size t -> extract (in_tuple (to_word (t0 :: t))) (nth set0 (tabrows (t0 :: t)) i.+1) = extract (in_tuple (to_word t)) (nth set0 (tabrows t) i).
proof: Proof. Proof using. move=> Hi. rewrite /tabrows /= /shiftset /= map_comp -!map_comp !extractIE. set f := (X in nth _ (map X _)). have /eq_map -> /= : f =1 (fun s => [set lsh_rec x | x in s]) \o (fun s => cast_set_tab t s). move=> S /=; rewrite /f {f} -setP => j. by apply/idP/idP; rewrite -!imset_comp /= -(eq_imset _ lcast_com) -!imset_comp. rewrite {f} /= enumIsize_to_word filter_cat map_cat -[RHS]cats0; congr (_ ++ _). - rewrite (nth_map set0) /=; last by rewrite size_shrows size_map. rewrite filter_map /= -map_comp. set f2 := (X in _ = map X _); rewrite (eq_map (g := f2)); first last. rewrite /f2 {f2} => j /=; rewrite !(tnth_nth inh) /=. by rewrite to_word_cons nth_cat ltn_ord. congr (map f2 _) => {f2}. apply: eq_filter => j /=; rewrite mem_imset; last exact lshift_recP. rewrite (nth_map set0) /cast_set_tab //=. by rewrite size_shrows size_map. - rewrite (eq_in_filter (a2 := pred0)); first by rewrite filter_pred0. move=> j' /mapP[j Hj /= -> {j'}]. apply/negP; rewrite (nth_map set0); last by rewrite size_shrows size_map. by move=> /imsetP[k _ /eqP]; rewrite eq_sym lrshift_recF. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype