{lem : ExcludedMiddle} (A : Ordinal) (P : A -> HProp) : merely (exists a, P a) -> merely (exists a, P a /\ forall b, P b -> a < b \/ a = b). Proof. intros H'. eapply merely_destruct; try apply H'. intros [a Ha]. induction (well_foundedness a) as [a _ IH]. destruct (LEM (merely (exists b, P b /\ b < a)) _) as [H|H]. - eapply merely_destruct; try apply H. intros [b Hb]. apply (IH b); apply Hb. - apply tr. exists a. split; try apply Ha. intros b Hb. specialize (trichotomy_ordinal a b). intros H1. eapply merely_destruct; try apply H1. intros [H2|H2]. { apply tr. by left. } eapply merely_destruct; try apply H2. intros [H3|H3]. { apply tr. by right. } apply Empty_rec, H, tr. exists b. by split. Qed.
From HoTT Require Import TruncType ExcludedMiddle Modalities.ReflectiveSubuniverse abstract_algebra. From HoTT Require Import Universes.Smallness. From HoTT Require Import Colimits.Quotient. From HoTT Require Import HSet.