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