proposition: Lemma cover_tabcols t : is_part (shape t) -> cover [set s | s \in tabcols t] = setT.
proof: Proof. Proof using. move=> Hpart. apply/eqP; rewrite eqEcard; apply/andP; split; first exact: subsetT. have -> : tabcols t = tabcolsk t (size (head [::] t)). by rewrite /tabcolsk /= -size_tabcols take_size. rewrite (size_cover_tabcolsk _ Hpart). rewrite cardsT card_ord size_to_word /size_tab. have: head 0 (shape t) <= (size (head [::] t)) by case t. elim: (shape t) Hpart => [// | p0 p IHp] /= /andP[Hhead Hpart] Hp0. rewrite big_cons; apply: leq_add. - by rewrite minnC /minn ltnNge Hp0 /=. - by apply: (IHp Hpart); have:= leq_trans Hhead Hp0; case p. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype