proposition: Corollary isfinite_isdec_lessthan (X:OrderedSet) : isfinite X -> ∏ (x y:X), decidable (x < y).
proof: Proof. intros i ? ?. apply isdeceq_isdec_lessthan. now apply isfinite_isdeceq. Defined.
imports: UniMath.Combinatorics.FiniteSets UniMath.Foundations.UnivalenceAxiom UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions