proposition: Lemma lsplit_rec_tab k : head 0 (shape t) <= size t0 -> cover [set lsplit_rec x | x in [set s in tabcolsk (t0 :: t) k]] = cover [set s in tabcolsk t k].
proof: Proof. Proof using. move => Hsize; rewrite cover_imset /tabcolsk /= tabcols_cons /cover /preimset. apply/setP/subset_eqP/andP; split; apply/subsetP => i. - move/bigcupP => [S0]; rewrite !inE. move/(mem_takeP set0) => [pos]. rewrite size_map size_enum_ord leq_min => /andP[Hpos Hpos0] ->. rewrite (nth_map (Ordinal Hpos0)); last by rewrite size_enum_ord. rewrite !inE lrshift_recF /= (mem_imset _ _ lshift_recP) nth_ord_ltn => Hi. apply/bigcupP; exists (nth set0 (tabcols t) (Ordinal Hpos0)); last exact Hi. rewrite inE; apply/(mem_takeP set0). exists pos; last by []. rewrite leq_min Hpos /=. case: (ltnP pos (size (tabcols t))) => //= H. by move: Hi; rewrite (nth_default _ H) in_set0. - move/bigcupP => [S0]; rewrite !inE => /(mem_takeP set0) [pos]. rewrite leq_min => [] /andP[Hpos Hpossz] -> Hi. have Hpos0 : pos < size t0. apply: (leq_trans Hpossz). rewrite size_tabcols. by move: Hsize; rewrite /shape; case t. apply/bigcupP. exists (rsh_rec (Ordinal Hpos0) |: [set lsh_rec x | x in nth set0 (tabcols t) (Ordinal Hpos0)]). + rewrite inE; apply/(mem_takeP set0). exists pos; first by rewrite size_map size_enum_ord leq_min Hpos. rewrite (nth_map (Ordinal Hpos0)); last by rewrite size_enum_ord. by rewrite nth_ord_ltn. + by rewrite !inE lrshift_recF /=; apply/imsetP; exists i. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype