Proposition cha_max_min_distributive {H : complete_heyting_algebra} (x y z : H) : (x ∧ (y ∨ z)) = ((x ∧ y) ∨ (x ∧ z)). Proof. use cha_le_antisymm. - rewrite cha_min_comm. use cha_from_le_exp. use cha_max_le_case. + use cha_to_le_exp. rewrite cha_min_comm. use cha_max_le_l. + use cha_to_le_exp. rewrite cha_min_comm. use cha_max_le_r. - use cha_min_le_case. + use cha_max_le_case. * apply cha_min_le_l. * apply cha_min_le_l. + use cha_max_le_case. * refine (cha_le_trans (cha_min_le_r _ _) _). apply cha_max_le_l. * refine (cha_le_trans (cha_min_le_r _ _) _). apply cha_max_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.