proposition: Lemma Exercise1_22u u v: open_r r u -> open_r r v -> inf (reg_open_order r) u v = open_bar r (u \cap v).
proof: Proof. move => ou ov. set (z := open_bar r (u \cap v)). have oi: (open_o r (u \cap v)). apply: Exercise1_22b => //; move=> x. case/set2_P => ->; [by case: ou | by case: ov]. move: (Exercise1_22i oi) (Exercise1_22e oi)=> oz sz. apply: inf_pr2. rewrite/reg_open_order; fprops. apply /Exercise1_22rP; split => //; rewrite (Exercise1_22p ou). apply: Exercise1_22j => //; [by case: ou | apply: subsetI2l]. apply Exercise1_22rP; split => //; rewrite (Exercise1_22p ov). apply: Exercise1_22j => //; [by case: ov | apply: subsetI2r]. move => t /Exercise1_22rP [ot _ tu] /Exercise1_22rP [_ _ tv]. apply /Exercise1_22rP; split => //. apply: (@sub_trans (u \cap v)) => //. by move=> w wt; apply: setI2_i; [apply: tu | apply: tv]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)