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