fact: Definition theSmallest {X : WellOrderedSet} (S : hsubtype X) : hProp := (∃ s, S s) ⇒ make_hProp (∑ s:X, S s ∧ ∀ t:X, S t ⇒ WOrel X s t)%type (isaprop_theSmallest _ (WO_isTotalOrder X) S).
imports: UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.Propositions UniMath.MoreFoundations.Subtypes UniMath.MoreFoundations.Sets UniMath.MoreFoundations.AxiomOfChoice UniMath.Combinatorics.OrderedSets