proposition: Lemma trivIset_tabrowsk k t : trivIset [set s | s \in (tabrowsk t k)].
proof: Proof. Proof using. apply: trivIs; rewrite /tabrowsk /tabrows /= -map_take. apply: trivIseq_map; first exact: cast_ord_inj. apply: (trivIsubseq (v := (shrows (shape t)))). - rewrite -{2}[shrows (shape t)](cat_take_drop k). exact: prefix_subseq. - exact: trivIseq_shrows. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype