proposition: Lemma Greene_rel_t_inf k : Greene_rel_t k >= minn N k.
proof: Proof. Proof using. pose P := [set [set i ] | i in Ik k]. have <- : #|cover P| = minn N k. rewrite /= (_ : cover P = Ik k); first exact: sizeIk. rewrite /cover {}/P. apply/setP => i; apply/bigcupP/idP => /= [[St /imsetP[j Hj -> {St}]] | Hi]. - by rewrite in_set1 => /eqP ->. - exists [set i]; last by rewrite in_set1. by apply/imsetP; exists i. have HP : P \is a k.-supp. rewrite /ksupp; apply/and3P; split. - rewrite card_imset; last exact: set1_inj. rewrite sizeIk; exact: geq_minr. - apply/trivIsetP => A B /imsetP[i Hi ->{A}] /imsetP[j Hj ->{B}]. rewrite inE in Hi; rewrite inE in Hj => Hneq. exact: set1_disjoint. - apply/forallP => s; apply/implyP => /imsetP[i Hi ->]; rewrite inE in Hi. by rewrite extract1 /sorted. by rewrite /Greene_rel_t; exact: (leq_bigmax_cond (F := (fun x => #|cover x|))). Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype