proposition: Lemma Exercise1_22g u: open_o r u -> cofinal (induced_order r (open_bar r u)) u.
proof: Proof. move=> ou; move:(Exercise1_22e ou) (Exercise1_22f ou) => h1 h2. apply /cofinal_inducedP => //; split => //. move => x /setU_P [y xy] /Zo_P [] /setP_P ysr [oy ]. move /(cofinal_inducedP ysr) => [uy h]; apply: (h _ xy). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)