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