proposition: Lemma Exercise1_22B F x: cofinal r F -> open_r r x -> open_r (induced_order r F) (x \cap F).
proof: Proof. move=> cf ox. have sF: (sub F (substrate r)) by case: cf. move: (iorder_osr or sF) => [oio sio]. have oioi: (open_o (induced_order r F) (x \cap F)). red; rewrite iorder_sr //; split; first by apply: subsetI2r. move=> a b /setI2_P [ax aF] ab. move: (iorder_gle1 ab)(iorder_gle3 ab) => leab [_ nF]. apply /setI2_P;split => //. move: ox => [[_ ox] _]; apply: (ox _ _ ax leab). split; first by exact. move=> v ov cfi. move: (proj1 ov); rewrite iorder_sr // => svF. move:(proj1 cfi); rewrite iorder_sr // ? iorder_sr // => siv. apply: extensionality =>// t tv. move: (ov) => [sov _]. move: sov; rewrite iorder_sr // => sov;move: cfi; rewrite iorder_trans //. move /(cofinal_inducedP (sub_trans sov sF)) => [_ cfi]. have tF: inc t F by apply: sov. move: sov => /setP_P sov. move: (sF _ tF) => ts. apply /setI2_P;split => //. rewrite (Exercise1_22p ox); apply: Exercise1_22h => //; first by case: ox. move => y ty. have ysr: inc y (substrate r) by order_tac. move: cf=> [_ cf]; move: (cf _ ysr) => [z zF yz]. have aux: (gle (induced_order r F) t z) by apply /iorder_gle0P => //; order_tac. move:ov => [_ h]; move: (h _ _ tv aux) => zv. move: (cfi _ zv)=> [w h1 h2]; move: h1 => /setI2_P [wx wf]; ex_tac; order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)