proposition: Lemma iso_graph_mon4 g1 g2 a b c d: inc g1 iso_graphs -> inc g2 iso_graphs -> inc (J a b) g1 -> inc (J c d) g2 -> (gle r1 a c <-> gle r2 b d).
proof: Proof. move: g1 g2 a b c d. move:(proj1 wor1) (proj1 wor2) => or1 or2. suff H: forall g1 g2 a b c d, inc g1 iso_graphs -> inc g2 iso_graphs -> inc (J a b) g1 -> inc (J c d) g2 -> gle r1 a c -> glt r2 d b -> False. move => g1 g2 a b c d g1i g2i ha hb. move: (g2i) => /Zo_S /setP_P pp. move/setXp_P:(pp _ hb) =>[csr dsr]. move: (g1i) => /Zo_S /setP_P pp1. move/setXp_P:(pp1 _ ha) =>[asr bsr]. split => le1. case : (total_order_pr2 (worder_total wor2) dsr bsr) => // gt. case: (H _ _ _ _ _ _ g1i g2i ha hb le1 gt). case : (total_order_pr2 (worder_total wor1) csr asr) => // gt. case: (equal_or_not b d ) => ebd; last first. case:(H g2 g1 c d a b g2i g1i hb ha (proj1 gt) (conj le1 ebd)). rewrite - ebd in hb. set Z := Zo (substrate r1) (fun c1 => exists a1 b1, [/\ inc (J a1 b1) g1, inc (J c1 b1) g2 & glt r1 c1 a1]). have nez: nonempty Z. exists c; apply: Zo_i; [ by order_tac | by exists a,b]. have sz: sub Z (substrate r1) by apply: Zo_S. apply: False_ind. clear a b c d asr bsr csr dsr ha hb le1 gt ebd. move: (worder_prop wor1 sz nez) =>[c /Zo_hi [a [b [abg cbg lt1]]] cm]. move: (iso_graph_mon2 g1i abg lt1) =>[d lt2 cdg]. move: (iso_graph_mon1 g2i cbg lt2) =>[e lt3 edg]. have /cm mt2: inc e Z. apply: Zo_i. order_tac. exists c, d. split => //. order_tac. move => g1 g2 a b c d g1i g2i abg cdg le1 lt1. set Z := Zo (substrate r2) (fun d1 => exists a1 b1 c1, [/\ inc (J a1 b1) g1, inc (J c1 d1) g2, gle r1 a1 c1& glt r2 d1 b1]). have neZ: nonempty Z. exists d; apply: Zo_i; [ by order_tac | by exists a,b,c]. have sz: sub Z (substrate r2) by apply: Zo_S. clear a b c d abg cdg le1 lt1. move: (worder_prop wor2 sz neZ) =>[d /Zo_hi [a [b [c [abg cdg le1 lt1]]]] cm]. move: (iso_graph_mon1 g1i abg lt1) =>[e hc lt3]. have lt4: glt r1 e c by order_tac. move:(iso_graph_mon2 g2i cdg lt4) =>[f lt5 hd ]. have /cm fz: inc f Z. apply: Zo_i; first by order_tac. exists e,d,e; split => //; order_tac. by move /setP_P: (Zo_S g2i) => h; move:(h _ hd) => /setXp_P []. order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)