proposition: Lemma Exercise1_2e2 r a b c (E:= substrate r) (s := (diagonal E) \cup (doubleton (J a c) (J c a))): order r -> glt r a b -> glt r b c -> [/\ equivalence s, substrate s = substrate r, ~ ( weak_order_compatibility r s) & ~ ( Ex1_2_hC' r s)].
proof: Proof. move => or lab lbc. have asr: inc a (substrate r) by order_tac. have csr: inc c (substrate r) by order_tac. have dp := (diagonal_i_P E); have dpi:= (diagonal_pi_P E). have gs: sgraph s by move => t /setU2_P [ /dp [] // | /set2_P [] ->]; fprops. have pa: forall u v, inc (J u v) s -> (inc u E /\ inc v E). move => u v;case/setU2_P; first by move/dp; aw; move=> [_ xE <-]. by case /set2_P => h;rewrite (pr1_def h) (pr2_def h). have pb: forall t, inc t E -> related s t t. by move => t te; apply /setU2_P; left; apply/dpi. have sr: substrate s = E. set_extens t; last by move /pb => h; substr_tac. by move /(substrate_P gs);case; move => [y /pa [tE tE']]. have sac: related s a c by apply /setU2_P; right; fprops. have sca: related s c a by apply /setU2_P; right; fprops. have es: equivalence s. split => //; first by red; rewrite sr => t; apply pb. move => x y z yx xz. case/setU2_P:(yx); [ by move/dp=> [_ _]; aw => -> | move => h1]. case/setU2_P:(xz); [ by move/dp=> [_ _]; aw => <- | move => h2]. case/set2_P: h1 => h1; rewrite ? (pr1_def h1) ? (pr2_def h1); case/set2_P:h2 => h2; rewrite ? (pr1_def h2) ? (pr2_def h2);fprops. move => x y xy;apply /setU2_P; case/setU2_P: xy. by move/dp;aw; move=> [_ ha <-]; left;apply /dpi. case/set2_P => h; rewrite (pr1_def h) (pr2_def h);fprops. move:(proj2 lab) (proj2 lbc) => nab nbc; move:(nesym nab) => nba. split => //. move => [_ pc]; move: (pc a b c (proj1 lab) sac) => [z]. case /setU2_P; first by move /dpi => [_ <-] => cb; order_tac. by case /set2_P => /pr1_def. move => hh; move: (hh a b c (proj1 lab) (proj1 lbc) sac). by case /setU2_P; [ move /dpi => [_ ] | case /set2_P => /pr2_def]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)