Proposition cha_min_max_distributive {H : complete_heyting_algebra} (x y z : H) : (x ∨ (y ∧ z)) = ((x ∨ y) ∧ (x ∨ z)). Proof. rewrite (cha_max_min_distributive (x ∨ y) x z). rewrite (cha_min_comm (x ∨ y) x). rewrite cha_min_absorb. rewrite (cha_min_comm (x ∨ y) z). rewrite cha_max_min_distributive. rewrite (cha_min_comm z y). rewrite <- cha_max_assoc. apply maponpaths_2. rewrite (cha_min_comm z x). rewrite (cha_max_absorb x z). apply idpath. 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.