proposition: Lemma Exercise1_22j u v: open_o r u -> open_o r v -> sub u v -> sub (open_bar r u) (open_bar r v).
proof: Proof. move=> ou ov uv. move=> t tu;apply: Exercise1_22h => //; first by apply: (Exercise1_22f ou). move: (Exercise1_22i ou) => [[ob1 ob2] _]. move=> y ty; move: (ob2 _ _ tu ty) => ybu. move: (Exercise1_22g ou) => /(cofinal_inducedP ob1) [_ h]. move: (h _ ybu) => [z zu yz]; exists z => //;fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)