Proposition min_op_l {X : Poset} (min : min_operation X) (x y : X) : min_op min x y ≤ x. Proof. exact (pr12 (min x y)). Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Lattice.Lattice. Require Import UniMath.OrderTheory.Lattice.Bounded.