proposition: Lemma trivIset_tabcolsk k t : trivIset [set s | s \in (tabcolsk t k)].
proof: Proof. Proof using. apply: trivIs; rewrite /tabcolsk /=. apply: (trivIsubseq (v := (tabcols t))); last exact: trivIseq_tabcols. rewrite -{2}[tabcols t](cat_take_drop k). exact: prefix_subseq. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype