fact: Definition isMaximal {X : Poset} (x : X) : UU := ∏ y, x ≤ y -> x = y.
imports: UniMath.Combinatorics.FiniteSets UniMath.Foundations.UnivalenceAxiom UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions