Require Import Prelude.

Implicit Types (x y z : nat) (p q : nat -> Prop).

Inductive Acc : nat -> Prop :=
| AccI x : (forall y, y < x -> Acc y) -> Acc x.

Fact comp_ind x :
  Acc x.
Proof.
  enough (forall y, y <= x -> Acc y) by eauto.
  induction x as [|x IH]; intros y H.
  - constructor. intros z H1. exfalso. omega.
  - constructor. intros z H1.
    apply IH. omega.
Qed.

Fact ex_least (XM : forall P, P \/ ~ P) p :
  ex p -> exists x, p x /\ forall y, p y -> x <= y.
Proof.
  intros [x H].
  induction (comp_ind x) as [x _ IH].
  destruct (XM (exists y, p y /\ y < x)) as [(y&H1&H2)|H1].
  - now apply (IH y).
  - exists x. split. exact H.
    intros y H2. contra XM H3.
    apply H1. exists y. split. exact H2. omega.
Qed.