proposition: Lemma Exercise1_22z: relatively_complemented (reg_open_order r).
proof: Proof. move: (Exercise1_22t) => lee. have oro: (order (reg_open_order r)) by rewrite /reg_open_order; fprops. have thel: (the_least (reg_open_order r) = emptyset). by apply: the_least_pr2. split => //; [by apply: Exercise1_22y | exists emptyset => // |]. move=> x y /Exercise1_22rP [ox oy xy]. move: (ox) (oy)=> [oox _] [ooy _]. set (z:= Zo y (fun u => forall t, gle r u t -> ~ (inc t x))). have zr: (sub z (substrate r)). apply: (@sub_trans y) ;[ apply: Zo_S | by case: (proj1 oy) ]. have oz: (open_o r z). split => //; move=> u v /Zo_P [uy h] uv; apply :Zo_i=> //. move:ooy => [aa h1]; apply: (h1 _ _ uy uv). by move=> t vt tx; case: (h _ (order_transitivity or uv vt)). move: (Exercise1_22i oz)=> orz. have ou: (open_o r (x \cup (open_bar r z))). by apply: Exercise1_22a =>//; move: orz; move=> [ok _]. exists (open_bar r z); red. rewrite thel Exercise1_22w // Exercise1_22u //. move: (Exercise1_22p ox)(Exercise1_22p oy) => bxp byp. have xze: (x \cap z) = emptyset. apply /set0_P; move=> a /setI2_P [ax] /Zo_P. move=> [ay h1]; case: (h1 a) => //; order_tac. by move: (oox) => [xsr _]; apply: xsr. have zy: sub z y by apply: Zo_S. split; first (by apply /Exercise1_22s1P); last first. rewrite bxp Exercise1_22k // - Exercise1_22p //; apply: Exercise1_22m=>//. apply: extensionality. rewrite byp;apply: Exercise1_22j => //. move=> t; case/setU2_P; first by apply: xy. rewrite byp; apply: (Exercise1_22j oz ooy zy). move: ooy=> [ysr ooy2]. move=> t ty; apply: Exercise1_22h =>//; first by apply: ysr. move=> u tu. move: (ooy2 _ _ ty tu) => uy. case: (p_or_not_p (exists2 t, inc t x & gle r u t)). by move=> [w wx uw]; exists w => //; apply: setU2_1. move: (ysr _ uy) => usr. move=> h; exists u => //; last (by order_tac); apply: setU2_2. apply: Exercise1_22e => //; apply: Zo_i => // w uw; case: (inc_or_not w x) =>//. by move=> wx; case: h; exists w. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)