Definition stnposet ( n : nat ) : Poset. Proof. unfold Poset. exists (_,,isasetstn n). unfold PartialOrder. exists (λ i j: ⟦n⟧, i ≤ j)%dnat. unfold isPartialOrder. split. - unfold ispreorder. split. * intros i j k. apply istransnatleh. * intros i. apply isreflnatleh. - intros i j r s. apply (invmaponpathsincl _ ( isinclstntonat _ )). apply isantisymmnatleh; assumption. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.Combinatorics.StandardFiniteSets.