Lemma WO_theUniqueSmallest {X : WellOrderedSet} (S : hsubtype X) : (∃ s, S s) ⇒ ∃! s:X, S s ∧ ∀ t:X, S t ⇒ s ≤ t. Proof. intros ne. apply iscontraprop1. - apply isaprop_theSmallest. apply WO_isTotalOrder. - exact (WO_theSmallest S ne). 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.