proposition: Lemma tabcols_cons : tabcols (t0 :: t) = [seq rsh_rec i |: (lsh_rec @: (nth set0 (tabcols t) i)) | i <- enum 'I_(size t0)].
proof: Proof. Proof using. rewrite /tabcols /cast_cons /=. apply: (@eq_from_nth _ set0); first by rewrite !size_map. move=> i; rewrite 2!size_map => Hienum; have:= Hienum; rewrite size_enum_ord => Hi. rewrite -map_comp (nth_map (Ordinal Hi)) //= !(nth_enum_ord _ Hi). rewrite (nth_map (Ordinal Hi)) //= !(nth_enum_ord _ Hi). rewrite imsetU1 -!imset_comp. case (ltnP i (size (shcols (shape t)))) => Hish. - rewrite (nth_map set0 _ _ Hish). have:= (rcast_com (nth (Ordinal Hi) (enum 'I_(size t0)) i)) => /= ->. by rewrite -!imset_comp (eq_imset _ lcast_com). - rewrite [nth set0 (map _ _) i](_ : _ = set0); first last. by rewrite nth_default //= size_map. rewrite [nth _ _ i](_ : _ = Ordinal Hi); first last. by apply: val_inj; rewrite /= nth_enum_ord. by rewrite nth_default //= !imset0 -(rcast_com (Ordinal Hi)). Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype