proposition: Lemma rsplit_rec_tab k : cover [set rsplit_rec x | x in [set s in (tabcolsk (t0 :: t)) k]] = [set i : 'I_(size t0) | i < k].
proof: Proof. Proof using. rewrite /tabcolsk /= tabcols_cons. apply/setP/subset_eqP/andP; split; apply/subsetP => i. - rewrite in_set /= /preimset. rewrite /cover => /bigcupP[sj /imsetP[stk]]. rewrite inE => /(mem_takeP set0) [j]. rewrite size_map size_enum_ord leq_min => [/andP[Hjk Hjt0]]. rewrite (nth_map (Ordinal Hjt0)); last by rewrite size_enum_ord. rewrite (nth_enum_ord _ Hjt0). rewrite (_ : nth _ _ _ = (Ordinal Hjt0)); first last. by apply/eqP; rewrite /eq_op /= nth_enum_ord. move=> -> -> {sj stk}; rewrite inE in_setU1 rshift_in_lshift_recF orbF. by move=> /eqP/rshift_recP ->. - rewrite inE /cover /preimset => Hi. apply/bigcupP; exists [set i]; last by rewrite in_set1. apply/imsetP; exists ((rsh_rec i) |: [set lsh_rec x | x in nth set0 (tabcols t) i]). + rewrite inE; apply/(mem_takeP set0). exists i; first by rewrite size_map size_enum_ord leq_min Hi ltn_ord. rewrite (nth_map i); last by rewrite size_enum_ord; apply: ltn_ord. rewrite nth_enum_ord; last exact: ltn_ord. by rewrite nth_ord_enum. + apply/setP/subset_eqP/andP; split; apply/subsetP => j; rewrite in_set1. * by move/eqP=> -> {j}; rewrite !inE eq_refl. * by rewrite !inE rshift_in_lshift_recF orbF => /eqP/rshift_recP ->. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype