proposition: Lemma Exercise1_22i u: open_o r u -> open_r r (open_bar r u).
proof: Proof. move=> ou. move: (Exercise1_22f ou) => sbu. have op: (open_o r (open_bar r u)). by apply: Exercise1_22c => //; move => x => /Zo_hi []. split => // v [sv ov] ; move: (Exercise1_22g ou). move /(cofinal_inducedP sbu) => [_ c]. move /(cofinal_inducedP sv) => [ss c']; apply: extensionality =>// t tv. apply: Exercise1_22h => //; first by apply: sv. move=> y ty; move: (ov _ _ tv ty) => yv; move: (c' _ yv) => [z zb zy]. move: (c _ zb) => [w wu zw]; ex_tac; order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)