Corollary isdeceq_isdec_lessthan (X:OrderedSet) : isdeceq X -> ∏ (x y:X), decidable (x < y). Proof. intros i ? ?. unfold Poset_lessthan. apply decidable_ishinh. apply decidable_dirprod. - now apply isdeceq_isdec_ordering. - apply neg_isdecprop. apply isdecpropif. * apply setproperty. * apply i. 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.