Lemma WOlt_trich (X : WellOrderedSet) (hX : isdeceq X) (x y : X) : y < x ∨ x = y ∨ x < y. Proof. induction (hX x y) as [Heq|Hneq]. - now apply hinhpr, inr, hinhpr, inl. - apply (squash_to_hProp (WO_istotal X x y)); intros [Hle|Hle]. + now apply hinhpr, inr, hinhpr, inr, WOlt'_to_WOlt. + apply hinhpr, inl, WOlt'_to_WOlt; split; trivial. now intros H; apply Hneq. Qed.
Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.Propositions. Require Import UniMath.MoreFoundations.Subtypes. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.AxiomOfChoice. Require Import UniMath.OrderTheory.OrderedSets.OrderedSets.