proposition: Lemma isaprop_theSmallest {X : hSet} (R : hrel X) (total : isTotalOrder R) (S : hsubtype X) : isaprop (∑ s:X, hProp_to_hSet (S s ∧ ∀ t:X, S t ⇒ R s t)).
proof: Proof. induction total as [[po anti] tot]. apply invproofirrelevance; intros s t. apply subtypePath_prop. induction s as [x i], t as [y j], i as [I i], j as [J j]. change (x=y)%logic. apply (squash_to_hProp (tot x y)); intros [c|c]. { apply anti. { exact c. } { exact (j x I). } } { apply anti. { exact (i y J). } { exact c. } } Defined.
imports: UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.Propositions UniMath.MoreFoundations.Subtypes UniMath.MoreFoundations.Sets UniMath.MoreFoundations.AxiomOfChoice UniMath.Combinatorics.OrderedSets