proposition: Theorem Greene_row_tab k t : is_tableau t -> Greene_row (to_word t) k = sumn (take k (shape t)).
proof: Proof. Proof using. move=> Htab; apply/eqP; rewrite eqn_leq; apply/andP; split. - rewrite -(conj_partK (is_part_sht Htab)) -sum_conj. rewrite (shape_tabcols Htab) /Greene_row /Greene_rel /Greene_rel_t. apply/bigmax_leqP => /= U; rewrite /ksupp => /and3P[Hsz Htriv]. have:= Htriv; rewrite /trivIset => /eqP <- /forallP/= Hall. under eq_bigr do rewrite -(tabcol_cut (is_part_sht Htab)). rewrite exchange_big /= big_map. rewrite !big_seq; apply: leq_sum. move=> /= V HV; rewrite leq_min; apply/andP; split. + exact: trivIset_I. + apply: (@leq_trans #|U|); last exact Hsz. rewrite -sum1_card; apply: leq_sum. move=> P HP; apply: size_row_extract => //=. by move/(_ P): Hall; rewrite HP. - rewrite /Greene_row /Greene_rel_t /= -(size_cover_tabrows _ (is_part_sht Htab)). apply: (leq_bigmax_cond (F := (fun x => #|cover x|))). exact: ksupp_leqX_tabrowsk. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype