proposition: Lemma ksupp_gt_tabcolsk k t : is_tableau t -> [set s | s \in (tabcolsk t k)] \is a k.-supp[>%O, in_tuple (to_word t)].
proof: Proof. Proof using. move=> Htab; rewrite /ksupp /tabcolsk; apply/and3P; split. - apply: (leq_trans (card_seq (tabcolsk t k))). by rewrite /tabcolsk /= size_take; exact: geq_minl. - exact: trivIset_tabcolsk. - apply/forallP => s; apply/implyP. rewrite /= inE => /mem_take Hin. rewrite -(nth_index set0 Hin). move: Hin; rewrite -index_mem; set i := index _ _ => Hi. exact: (sorted_gt_tabcols Htab). Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype