Definition standardFiniteOrderedSet (n:nat) : FiniteOrderedSet. Proof. intros. simple refine (_,,_). - exists (stnposet n). intros x y; apply istotalnatleh. - apply isfinitestn. 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.