Proposition max_op_l {X : Poset} (max : max_operation X) (x y : X) : x ≤ max_op max x y. Proof. exact (pr12 (max x y)). Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Lattice.Lattice. Require Import UniMath.OrderTheory.Lattice.Bounded.