Proposition le_min_op {X : Poset} (min : min_operation X) {x y z : X} (p : z ≤ x) (q : z ≤ y) : z ≤ min_op min x y. Proof. exact (pr222 (min x y) z p q). Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Lattice.Lattice. Require Import UniMath.OrderTheory.Lattice.Bounded.