proposition: Lemma Exercise2_1a r x y (E := substrate r) (r':= r \cup (Zo (coarse E)(fun z=> gle r (P z) x /\ gle r y (Q z)))): order r -> inc x (substrate r) -> inc y (substrate r) -> ~ gle r y x -> (gle (finer_order E) r r' /\ inc (J x y) r').
proof: Proof. move=> or xsr ysr h; split; last first. apply: setU2_2; apply:Zo_i; first by apply:inc_coarse. by saw; order_tac. apply/fo_gleP. have gr: sgraph r by fprops. have gr': sgraph r'. by move=> t /setU2_P; case; [ apply: gr | move => /Zo_P [] /setX_P []]. have sr1: forall a b, inc (J a b) r' -> (inc a E /\ inc b E). move => a b; case /setU2_P; first by move => pr; rewrite /E; split;substr_tac. by move => /Zo_S/setXp_P. have sr': substrate r' = E. set_extens t. by move /(substrate_P gr');case; move => [z si]; case: (sr1 _ _ si). by move => tE; apply: (@arg1_sr r' t t); apply /setU2_P; left; order_tac. split => //; last by apply: subsetU2l. split => //. by move => a; rewrite sr' => aE; apply: setU2_1; order_tac. move => a b c pa pb. have ae: inc a E by rewrite - sr'; substr_tac. have be: inc b E by rewrite - sr'; substr_tac. have ce: inc c E by rewrite - sr'; substr_tac. have jc: inc (J b c) (coarse E) by apply : inc_coarse. case /setU2_P : pa=> pa. case /setU2_P: pb => pb; first by apply /setU2_P; left; order_tac. apply /setU2_P; right;apply /Zo_P; saw. move /Zo_P: pb => [pb []]; aw; rewrite /gle/related => pc pd. split => //;order_tac. apply /setU2_P; right;apply /Zo_P; saw. move /Zo_P: pa => [pa []]; aw; rewrite /gle/related => pc pd. case /setU2_P: pb => pb; first by split => //; order_tac. move /Zo_P: pb => [pb []]; aw; rewrite /gle/related => pe pf. split => //; order_tac. move => a b pa pb. case /setU2_P : pa=> pa. case /setU2_P: pb => pb; first by order_tac. move /Zo_P: pb => [pb []]; aw => pc pd; case: h. have ab:gle r a b by done. have ax:gle r a x by order_tac. order_tac. move /Zo_P: pa => [pa []]; aw => qa qb. case /setU2_P: pb => pb; case: h. have ab:gle r b a by done. have ax:gle r y a by order_tac. order_tac. move /Zo_P: pb => [pb []]; aw => pc pd; order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)