proposition: Lemma shape_tabcols t: is_tableau t -> conj_part (shape t) = [seq #|s : {set 'I_(size (to_word t))}| | s <- tabcols t].
proof: Proof. Proof using. move=> Htab. rewrite -shcol_cards; last exact: is_part_sht. rewrite /tabcols; apply: (@eq_from_nth _ 0). - by rewrite !size_map size_shcols; case t. - move => i; rewrite size_map => Hi. have Hihead : i < size (head [::] t). by move: Hi; rewrite size_shcols /shape /=; case t. rewrite -map_comp !(nth_map set0 _ _ Hi) /=. by rewrite card_imset; last exact: cast_ord_inj. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype