proposition: Theorem Greene_col_tab k t : is_tableau t -> Greene_col (to_word t) k = sumn (take k (conj_part (shape t))).
proof: Proof. Proof using. move=> Htab; rewrite -sum_conj. apply/eqP; rewrite eqn_leq /=; apply/andP; split. - elim: t Htab => [_ | t0 t IHt] /=. by apply: (@leq_trans 0); first exact: Greene_rel_t_sup. move=> /and4P[_ Hrow _ /IHt{IHt} Ht]; rewrite to_word_cons. apply: (@leq_trans (Greene_col (in_tuple (to_word t)) k + Greene_col (in_tuple t0) k)). + by apply: Greene_rel_cat => a b c /= H1 H2; apply: (lt_trans H2 H1). + rewrite big_cons addnC; apply: leq_add; last exact Ht. have:= (@Greene_rel_seq _ >%O _ t0 k). rewrite /Greene_rel /= => -> //=. * by move=> a b c /=; rewrite -!leNgt; exact: le_trans. * move: Hrow; rewrite /sorted; case: t0 => [// | l t0]. rewrite (eq_path (e' := fun a b => ~~ (b < a)%O)) // => i j /=. exact: leNgt. - rewrite /Greene_rel_t /= -(size_cover_tabcolsk _ (is_part_sht Htab)). apply: (leq_bigmax_cond (F := (fun x => #|cover x|))). exact: ksupp_gt_tabcolsk. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype