proposition: Theorem Erdos_Szekeres (disp : unit) (T : inhOrderType disp) (m n : nat) (s : seq T) : size s > m * n -> (exists t, subseq t s /\ sorted <=%O t /\ size t > m) \/ (exists t, subseq t s /\ sorted >%O t /\ size t > n).
proof: Proof. Proof using . move=> Hsize; pose tab := RS s. have {Hsize} : (n < size (shape tab)) \/ (m < head 0 (shape tab)). have Hpart := is_part_sht (is_tableau_RS s). apply/orP; move: Hsize; rewrite -(size_RS s) /size_tab. apply contraLR; rewrite negb_or -!leqNgt => /andP[Hn Hm]. exact: (leq_trans (part_sumn_rectangle Hpart) (leq_mul _ _)). move=> [] Hltn. - right => {m}. have := Greene_col_RS 1 s. rewrite -sum_conj. rewrite (_ : \sum_(l <- _) minn l 1 = size (shape (RS s))); first last. have := is_part_sht (is_tableau_RS s). move: (shape _) => sh. elim: sh => [// | s0 sh IHsh Hpart]; first by rewrite big_nil. have /= Hs0 := part_head_non0 Hpart. move: Hpart => /= /andP[Hhead Hpart]. rewrite big_cons (IHsh Hpart) (_ : minn s0 1 = 1) ?add1n //. by case: s0 Hs0 {Hhead}. move: Hltn => /[swap] <-{tab}. case: (Greene_rel_one s >%O) => x [Hsubs] [Hsort <- Hn]. by exists x. - left => {n}. have := Greene_row_RS 1 s. rewrite (_ : sumn _ = head 0 (shape (RS s))); first last. by case: (shape (RS s)) => [| s0 l] //=; rewrite take0 addn0. rewrite /Greene_row; move: Hltn => /[swap] <-{tab}. case: (Greene_rel_one s <=%O) => x [Hsubs] [Hsort <- Hn]. by exists x. 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