Proposition max_op_le {X : Poset} (max : max_operation X) {x y z : X} (p : x ≤ z) (q : y ≤ z) : max_op max x y ≤ z. Proof. exact (pr222 (max x y) z p q). Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Lattice.Lattice. Require Import UniMath.OrderTheory.Lattice.Bounded.