proposition: Lemma ordinal_has_minimal_hsolutions {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: 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. now left. } eapply merely_destruct; try apply H2. intros [H3|H3]. { apply tr. now right. } apply Empty_rec, H, tr. exists b. now split. Qed.
imports: HoTT(TruncType ExcludedMiddle Modalities.ReflectiveSubuniverse abstract_algebra) HoTT(PropResizing.PropResizing) HoTT(Colimits.Quotient) HoTT(HSet)