Lemma isdeceq_isdec_ordering (X:OrderedSet) : isdeceq X -> isdec_ordering X. Proof. intros deceq ? ?. assert (tot := OrderedSet_istotal x y). induction (deceq x y) as [j|j]. - apply ii1. induction j. unwrap_OrderedSet X. apply refl. - assert (c : (y ≥ x) ⨿ (x ≥ y)). { assert (d : isaprop ((y ≥ x) ⨿ (x ≥ y))). { apply isapropcoprod. * apply propproperty. * apply propproperty. * intros r s. apply j; clear j. unwrap_OrderedSet X. now apply antisymm. } apply (squash_to_prop tot). + exact d. + intro e. exact e. } induction c as [c|c']. + now apply ii1. + apply ii2. intro le. apply j. now apply OrderedSet_isantisymm. 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.