proposition: Lemma WOlt_to_WOlt' (X : WellOrderedSet) (hX : isdeceq X) (x y : X) : x < y → WOlt' X x y.
proof: 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.
imports: UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.Propositions UniMath.MoreFoundations.Subtypes UniMath.MoreFoundations.Sets UniMath.MoreFoundations.AxiomOfChoice UniMath.Combinatorics.OrderedSets