Lemma WOlt_istrans (X : WellOrderedSet) : istrans (@WOlt X). Proof. intros x y z H1 H2 H3; simpl in *. apply (@squash_to_hProp _ (_,,isapropempty) (WO_istotal X y z)); intros [H|H]; simpl. - now apply H1, (WO_istrans X y z x H H3). - now apply H2. 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.