Proposition is_min_min_el {X : Poset} (m : min_el X) (y : X) : m ≤ y. Proof. exact (pr2 m y). Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Lattice.Lattice. Require Import UniMath.OrderTheory.Lattice.Bounded.