proposition: Lemma Erdos_Szerkeres r n m f (D := csucc (n *c m)) : total_order r -> natp n -> natp m -> fgraph f -> domain f = D -> sub (range f) (substrate r) -> {inc D &, injective (Vg f)} -> (exists B, [/\ sub B D, cardinal B = csucc m & forall i j, inc i B -> inc j B -> i <c j -> glt r (Vg f j) (Vg f i)]) \/ exists A, [/\ sub A D, cardinal A = csucc n & forall i j, inc i A -> inc j A -> i <c j -> glt r (Vg f i) (Vg f j)].
proof: Proof. move => [or tor] nN mN fgf df rgf injf. move: (NS_succ (NS_prod nN mN)); rewrite -/D => DN. pose comp i j := i <=c j /\ gle r (Vg f i) (Vg f j). pose cp := graph_on comp D. have: order_r comp. split. by move => i j k [ha hb] [hc hd]; split; [ apply: (cleT ha hc)| order_tac]. by move => i j [ha hb][hc hd]; apply: cleA. move => i j [[ha hb _] hc]; move: (arg1_sr hc) (arg2_sr hc) => ue ve. by split; split; try order_tac => //; apply: cleR. move/(order_from_rel D); rewrite -/cp => or1. have sr1: substrate cp = D. apply:graph_on_sr=> a aD;split. by apply: cleR;move/(NltP DN):aD => /proj31_1. order_tac;apply: rgf;apply: inc_V_range => //; ue. have csr1: cardinal (substrate cp) = csucc (n *c m) by rewrite sr1 card_nat. case: (Dilworth_lemma_v2 or1 nN mN csr1). move => [B /Zo_P [/setP_P sb pb] cb]; left; exists B; split => //; first ue. move => i j iB jB [cij nij]; split; last first. rewrite sr1 in sb;move => bad; case:nij. by rewrite (injf j i (sb _ jB) (sb _ iB) bad). rewrite sr1 in sb. have jsr: inc (Vg f j) (substrate r). by apply: rgf; apply: inc_V_range => //; rewrite df; apply: sb. have isr: inc (Vg f i) (substrate r). by apply: rgf; apply: inc_V_range => //; rewrite df; apply: sb. case: (tor (Vg f j) (Vg f i) jsr isr) => // ler. have h: gle cp i j by apply/graph_on_P1; split => //; apply: sb. case: nij; exact: (pb i j iB jB h). move => [A /total_subordersP [Asr tor1] xA]; right;exists A. have AD: sub A D by move: Asr; ue. split => // i j iA jA [lik nij]; split. move: (proj2 tor1 i j); rewrite iorder_sr // => h. move: (h iA jA); case; move/iorder_gle1 /graph_on_P1. by move => [_ _ [pa pb]] //. by move => [_ _ [pa pb]]; case: nij; apply: cleA. move => bad; case:nij. exact:(injf i j (AD _ iA) (AD _ jA) bad). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)