Lemma isaprop_isSmallest {X : Poset} (x : X) : isaprop (isSmallest x). Proof. intros. unfold isSmallest. apply impred_prop. Defined.
Require Import UniMath.Combinatorics.FiniteSets. Require Import UniMath.Foundations.UnivalenceAxiom. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.OrderTheory.Posets.Examples.StandardFiniteSet.