proposition: Lemma Exercise1_22k u v: open_o r u -> open_o r v -> disjoint u v -> disjoint (open_bar r u) (open_bar r v).
proof: Proof. rewrite /disjoint;move=> ou ov iuve; apply /set0_P. move=> y /setI2_P [] /setU_P [z yz z1] /setU_P [z' yz' z2]. move: z1 z2 => /Zo_P [] /setP_P z1 [[_ o1] c1] /Zo_P [] /setP_P z2 [[_ o2] c2]. move: c1 c2 => /(cofinal_inducedP z1) [uz c1]/(cofinal_inducedP z2)[vz' c2]. move: (c1 _ yz)=> [y1 y1u le1]. move: (c2 _ (o2 _ _ yz' le1)) => [y2 y2u le2]. empty_tac1 y2; apply: setI2_i => //. move: ou => [_ ou]; exact: (ou _ _ y1u le2). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)