proposition: Lemma WO_theSmallest {X : WellOrderedSet} (S : hsubtype X) : theSmallest S.
proof: Proof. intros ne. apply (squash_to_hProp (WO_hasSmallest X S ne)). intro c. exact c. Defined.
imports: UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.Propositions UniMath.MoreFoundations.Subtypes UniMath.MoreFoundations.Sets UniMath.MoreFoundations.AxiomOfChoice UniMath.Combinatorics.OrderedSets