Lemma WO_theSmallest {X : WellOrderedSet} (S : hsubtype X) : theSmallest S. Proof. intros ne. apply (squash_to_hProp (WO_hasSmallest X S ne)). intro c. exact c. Defined.
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.