proposition: Lemma Greene_rel_seq r k : sorted negR r -> Greene_rel r k = minn (size r) k.
proof: Proof. Proof using HnegR. move=> Hrow /=. apply/eqP; rewrite eqn_leq; apply/andP; split; last exact: Greene_rel_t_inf. rewrite leq_min Greene_rel_t_sup /=; apply/bigmax_leqP => s. rewrite /ksupp /trivIset => /and3P[Hcard /eqP /= <- /forallP Hsort]. suff {Hcard} H B : B \in s -> #|B| <= 1. apply: (@leq_trans (\sum_(B in s) 1)); last by rewrite sum1_card. exact: leq_sum. rewrite -(size_extract (in_tuple r)) /=. move=> HB; move/(_ B): Hsort; rewrite {}HB {s} /=. set s := (extractpred _ _) => Hsort. have : sorted negR s. move: Hrow; apply: (subseq_sorted HnegR); last exact: extsubsm. case H : s Hsort => [// | s0 [// | s1 tls]] /= /andP[Hgt _] /andP[]. by rewrite /negR Hgt. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype