proposition: Lemma WO_theUniqueSmallest {X : WellOrderedSet} (S : hsubtype X) : (∃ s, S s) ⇒ ∃! s:X, S s ∧ ∀ t:X, S t ⇒ s ≤ t.
proof: Proof. intros ne. apply iscontraprop1. - apply isaprop_theSmallest. apply WO_isTotalOrder. - exact (WO_theSmallest S ne). Defined.
imports: UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.Propositions UniMath.MoreFoundations.Subtypes UniMath.MoreFoundations.Sets UniMath.MoreFoundations.AxiomOfChoice UniMath.Combinatorics.OrderedSets