proposition: Lemma Exercise1_22A: boolean_lattice (reg_open_order r).
proof: Proof. move: (Exercise1_22t) => le. have oo: (order (reg_open_order r)) by rewrite /reg_open_order; fprops. split; first by apply: Exercise1_22z. by exists (substrate r); apply: (Exercise1_22s). move: (Exercise1_22y)=> lr. apply/ (distributive_lattice_prop3 lr) => x y z xsr ysr zsr. set (a1:= sup (reg_open_order r) x y). set (a2:= inf (reg_open_order r) y z). have a1s: (inc a1 (substrate (reg_open_order r))). move: (lattice_sup_pr lr xsr ysr) => [ok _ _]; order_tac. have a2s: (inc a2 (substrate (reg_open_order r))). move: (lattice_inf_pr lr ysr zsr) => [ok _ _]; order_tac. have b1s: inc (inf (reg_open_order r) z a1) (substrate (reg_open_order r)). move: (lattice_inf_pr lr zsr a1s) => [ok _ _]; order_tac. have b2s: inc (sup (reg_open_order r) x a2) (substrate (reg_open_order r)). move: (lattice_sup_pr lr xsr a2s) => [ok _ _]; order_tac. move: xsr ysr zsr a1s a2s b1s b2s =>/Exercise1_22s1P xor /Exercise1_22s1P yor /Exercise1_22s1P zor /Exercise1_22s1P a1or /Exercise1_22s1P a2or /Exercise1_22s1P b1or /Exercise1_22s1P b2or. apply /Exercise1_22rP; split => //. move: (refl_equal a1)(refl_equal a2); rewrite {2} /a1 {2} /a2. rewrite Exercise1_22u // Exercise1_22w// => a1s a2s. rewrite Exercise1_22u// Exercise1_22w// a1s a2s. move => a /setU_P [b ab] /Zo_P [] /setP_P bsr [[_ ob]]. move /(cofinal_inducedP bsr) => [bi bip]. move: (bsr _ ab) => asr. move: (xor)(yor)(zor) => [xo _] [yo _][zo _]. apply: Exercise1_22h => //. apply: Exercise1_22a => //; rewrite -a2s; by case: a2or. move=> c ac; move: (ob _ _ ab ac) => cb. move: (bip _ cb) => [d] /setI2_P [dz dbu] cd. move: dbu => /setU_P [e de] /Zo_P [] /setP_P esr [[_ oe]]. move /(cofinal_inducedP esr)=> [ei eip]. move: (eip _ de) => [f fxy ef]. exists f; last by order_tac. case/setU2_P: fxy => fx; first by apply: setU2_1. apply: setU2_2; apply: Exercise1_22e => //. by apply: Exercise1_22b => //; move=> i; case/set2_P => ->. apply: setI2_i => //. move: zo => [_ zo]; apply: (zo _ _ dz ef). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)