proposition: Corollary isfinite_isdec_ordering (X:OrderedSet) : isfinite X -> isdec_ordering X.
proof: Proof. intros i ? ?. apply isdeceq_isdec_ordering. now apply isfinite_isdeceq. Defined.
imports: UniMath.Combinatorics.FiniteSets UniMath.Foundations.UnivalenceAxiom UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions