proposition: Lemma Exercise1_22e u: open_o r u -> sub u (open_bar r u).
proof: Proof. move=> ou t tu; move: (ou) => [ou1 ou2]; apply: (@setU_i _ u) => //. apply: Zo_i; [by apply /setP_P | split => //; split; rewrite iorder_sr // ]. by move=> x xu; ex_tac; apply /iorder_gle0P => //; order_tac; apply: ou1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)