proposition: Corollary isdeceq_isdec_lessthan (X:OrderedSet) : isdeceq X -> ∏ (x y:X), decidable (x < y).
proof: 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.
imports: UniMath.Combinatorics.FiniteSets UniMath.Foundations.UnivalenceAxiom UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions