Proposition is_boolean_regular_element_cha (H : complete_heyting_algebra) : is_boolean_algebra (regular_element_cha H). Proof. intros x. use eq_regular_element ; cbn in x. refine (_ @ cha_not_not_lem x). cbn -[Lle]. use cha_le_antisymm. - use cha_not_not_monotone. use cha_max_le_max_r. use cha_glb_le. + refine (not_regular_element x ,, _). intro i. induction i as [ w Hw ]. use to_le_regular_element_lattice ; cbn. use cha_to_le_exp. exact Hw. + cbn. apply cha_le_refl. - use cha_not_not_monotone. use cha_max_le_max_r. use cha_le_glb. intros i. induction i as [ w Hw ] ; cbn. refine (from_le_regular_element_lattice (Hw (not_regular_element x ,, _))). cbn. apply cha_not_eval. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.BinaryOperations. Require Import UniMath.OrderTheory.Lattice.Lattice. Require Import UniMath.OrderTheory.Lattice.Bounded. Require Import UniMath.OrderTheory.Lattice.Heyting. Require Import UniMath.OrderTheory.Lattice.CompleteHeyting. Require Import UniMath.OrderTheory.Lattice.DerivedLawsCompleteHeyting.