proposition: Lemma Exercise1_22h u x: open_o r u -> inc x (substrate r) -> (forall y, gle r x y -> exists2 z, inc z u & gle r y z) -> inc x (open_bar r u).
proof: Proof. move=> ou xsr xp. move: (Exercise1_22f ou) => Ha. set (t:=(open_bar r u) \cup (Zo (substrate r) (fun z=> gle r x z))). have tsr: (sub t (substrate r)). move=> v; case/setU2_P; [ apply: Ha |apply: Zo_S]. apply: (@setU_i _ t). by apply: setU2_2; apply: Zo_i =>//; order_tac. have ob: (open_o r (open_bar r u)). by apply: Exercise1_22c => //;move=> v /Zo_hi []. apply: Zo_i; [by apply /setP_P | split]. apply:Exercise1_22a => //; split; first by apply: Zo_S. move=> a b => /Zo_P [asr xa] ab; apply: Zo_i; order_tac. move: (Exercise1_22g ou) => /(cofinal_inducedP Ha) [ubu c1]. have sut: sub u t by move => s su; apply /setU2_P; left; apply: ubu. apply/(cofinal_inducedP tsr); split => // a iat. case/setU2_P: (iat) => h; first by move: (c1 _ h). by move: h =>/Zo_P [pa pb]; move : (xp _ pb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)