Definition max_op {X : Poset} (max : max_operation X) (x y : X) : X := pr1 (max x y).
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Lattice.Lattice. Require Import UniMath.OrderTheory.Lattice.Bounded.