Proposition cha_conj_not {H : complete_heyting_algebra} (x y : H) : (¬x ∧ ¬y) = ¬(x ∨ y). Proof. use cha_le_antisymm. - use cha_to_le_exp. rewrite cha_min_comm. use cha_from_le_exp. use cha_max_le_case. + use cha_to_le_exp. refine (cha_le_trans _ _). { exact (cha_and_monotone_r (cha_min_le_l _ _)). } rewrite cha_min_comm. use cha_exp_eval. + use cha_to_le_exp. refine (cha_le_trans _ _). { exact (cha_and_monotone_r (cha_min_le_r _ _)). } rewrite cha_min_comm. use cha_exp_eval. - use cha_min_le_case. + use cha_to_le_exp. refine (cha_le_trans _ _). { refine (cha_and_monotone_r _). exact (cha_max_le_l x y). } use cha_exp_eval. + use cha_to_le_exp. refine (cha_le_trans _ _). { refine (cha_and_monotone_r _). exact (cha_max_le_r x y). } use cha_exp_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.