Corollary isfinite_isdec_ordering (X:OrderedSet) : isfinite X -> isdec_ordering X. Proof. intros i ? ?. apply isdeceq_isdec_ordering. now apply isfinite_isdeceq. 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.