Proposition cha_max_le_max_l {H : complete_heyting_algebra} {x₁ x₂ : H} (p : x₁ ≤ x₂) (y : H) : (x₁ ∨ y) ≤ (x₂ ∨ y). Proof. use cha_max_le_case. - refine (cha_le_trans p _). apply cha_max_le_l. - 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.