Proposition cha_not_not_conj {H : complete_heyting_algebra} (x y : H) : ¬ ¬(x ∧ y) = (¬ ¬ x ∧ ¬ ¬ y). Proof. use cha_le_antisymm. - use cha_min_le_case. + use cha_not_not_monotone. apply cha_min_le_l. + use cha_not_not_monotone. apply cha_min_le_r. - use cha_to_le_exp. refine (cha_le_trans _ (cha_not_eval (¬ x))). use cha_min_le_case. + refine (cha_le_trans (cha_min_le_l _ _) _). use cha_min_le_l. + use cha_to_le_exp. refine (cha_le_trans _ (cha_not_eval (¬ y))). use cha_min_le_case. * refine (cha_le_trans (cha_min_le_l _ _) _). refine (cha_le_trans (cha_min_le_l _ _) _). use cha_min_le_r. * use cha_to_le_exp. refine (cha_le_trans _ (cha_not_eval (x ∧ y))). use cha_min_le_case. ** refine (cha_le_trans (cha_min_le_l _ _) _). refine (cha_le_trans (cha_min_le_l _ _) _). use cha_min_le_r. ** use cha_min_le_case. *** refine (cha_le_trans (cha_min_le_l _ _) _). use cha_min_le_r. *** use cha_min_le_r. 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.