proposition: Lemma isaprop_isSmallest {X : Poset} (x : X) : isaprop (isSmallest x).
proof: Proof. intros. unfold isSmallest. apply impred_prop. Defined.
imports: UniMath.Combinatorics.FiniteSets UniMath.Foundations.UnivalenceAxiom UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions