proposition: Lemma Greene_rel_t_sup k : Greene_rel_t k <= N.
proof: Proof. Proof using. rewrite /Greene_rel_t /=; apply/bigmax_leqP => P _. move: (cover P) => cover {P}; rewrite -[N in _ <= N]card_ord. exact: max_card. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype