proposition: Lemma Exercise2_8b r a F: order r -> (inc F (Exercise2_8a_R r a) <-> [/\ sub F (substrate r), forall x y, glt r x y -> inc x F -> inc y F -> exists z, [/\ glt r x z, ~ gle r y z, ~ gle r z y & inc z F], inc a F & (forall z, inc z F -> gle r a z)]).
proof: Proof. move=> or; split. move => /Zo_P [] /setP_P Fd [p1 p2]. move: (p2) => []; rewrite iorder_sr // => pa pb. have pb': forall z , inc z F -> gle r a z. by move => z zf; move /iorder_gleP: (pb _ zf) => [_ _]. split => // x y xy xF yF. have xy': glt (induced_order r F) x y by apply /iorder_gltP. move: (p1 _ _ xy'); move=> [z []] /iorder_gltP [_ zF xz] /iorder_gleP p4 /iorder_gleP p5; exists z; split => // h; [ by case: p4 | by case: p5]. move=> [pF p1 p2 p3]; apply: Zo_i; first by apply /setP_P. split; last by split; rewrite iorder_sr // => x xF;apply /iorder_gle0P=> //; apply: p3. move=> x y; move/iorder_gltP =>[xF yF xy]. move: (p1 _ _ xy xF yF) => [z [z1 z2 z3 z4]]; exists z;split. by apply /iorder_gltP. by move /iorder_gleP => [_ _]. by move /iorder_gleP => [_ _]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)