proposition: Lemma Greene_rel_one (T : eqType) (s : seq T) (R : rel T) : exists t : seq T, subseq t s /\ sorted R t /\ size t = (Greene_rel R s) 1.
proof: Proof. Proof using . rewrite /Greene_rel /= /Greene_rel_t. set P := (X in \max_(_ | X _) _). have : #|P| > 0. apply/card_gt0P; exists set0. rewrite {}/P /ksupp !unfold_in /= cards0 /=. apply/andP; split. + by apply/trivIsetP => s1 s2; rewrite inE. + by apply/forallP => x; rewrite inE. rewrite {}/P => /(eq_bigmax_cond (fun x => #|cover x|)). case=> U /[swap] /[dup] Hmax ->. rewrite /ksupp unfold_in => /and3P[Hcard _ /forallP Hall]. case HU: #|U| => [/= | c]. move: HU => /eqP; rewrite cards_eq0 => /eqP ->. exists [::]; repeat split; first exact: sub0seq. by rewrite /cover big_set0 cards0. have {Hcard HU} : #|U| == 1. by move: Hcard; rewrite HU ltnS leqn0 => /eqP ->. move/cards1P => [x Hx]; subst U. move/(_ x) : Hall; rewrite inE eq_refl /=. set sol := extractpred _ _ => Hsol. exists sol; repeat split. + exact: extsubsm. + exact: Hsol. + by rewrite /sol size_extract /= /cover big_set1. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(tuple finfun finset bigop path order) partition tableau Schensted ordtype Greene Greene_inv