proposition: Lemma cover_tabcols_rec k : head 0 (shape t) <= size t0 -> cover [set s in (tabcolsk (t0 :: t) k)] = rsh_rec @: [set s : 'I_(size t0) | s < k] :|: lsh_rec @: cover [set s in (tabcolsk t k)].
proof: Proof. Proof using. move => Hsize. by rewrite split_rec_cover setUC rsplit_rec_tab (lsplit_rec_tab _ Hsize). Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype