Lemma WOlt_to_WOlt' (X : WellOrderedSet) (hX : isdeceq X) (x y : X) : x < y → WOlt' X x y. Proof. intros H. apply (squash_to_hProp (WO_istotal X x y)); intros [Hle|Hle]; simpl. - induction (hX x y) as [Heq|Hneq]. + rewrite Heq in H. induction (WOlt_isirrefl _ _ H). + now split. - induction (H Hle). 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.