Require Import Arith Lia.

Set Implicit Arguments.

Set Default Proof Using "Type".

Section nat_rev_ind.


  Variables (P : Prop)
            (HP : n, P (S n) P n).

  Theorem nat_rev_ind x y : x y P y P x.
  Proof using HP. induction 1; auto. Qed.

End nat_rev_ind.

Section nat_rev_ind'.


  Variables (P : Prop) (k : )
            (HP : n, n < k P (S n) P n).

  Theorem nat_rev_ind' x y : x y k P y P x.
  Proof using HP.
    intros .
    set (Q n := n k P n).
    assert ( x y, x y Q y Q x) as H.
      apply nat_rev_ind.
      intros n ( & ); split.
      .
      revert ; apply HP, .
    apply (H x y).
    .
    split; auto; .
  Qed.

End nat_rev_ind'.

Section minimizer_pred.

  Variable (P : Prop)
           (HP : p: { n | P n P n }, { P (proj1_sig p) } + { P (proj1_sig p) }).

  Definition minimizer n := P n i, i < n P i.

  Inductive bar n : Prop :=
    | in_bar_0 : P n bar n
    | in_bar_1 : P n bar (S n) bar n.

  Let bar_ex n : bar n P n P n.
  Proof. induction 1; auto. Qed.

  Let loop : n, bar n { k | P k i, n i < k P i }.
  Proof.
    refine (fix loop n Hn { struct Hn } := match HP (exist _ n (bar_ex Hn)) with
      | left H exist _ n _
      | right H match loop (S n) _ with
        | exist _ k Hk exist _ k _
      end
    end).
    * split; auto; intros; .
    * destruct Hn; [ destruct H | ]; assumption.
    * destruct Hk as ( & ).
      split; trivial; intros i Hi.
      destruct (eq_nat_dec i n).
      - subst; trivial.
      - apply ; .
  Qed.

  Hypothesis Hmin : ex minimizer.

  Let : bar 0.
  Proof.
    destruct Hmin as (k & & ).
    apply in_bar_0 in .
    clear HP.
    revert .
    apply nat_rev_ind' with (k := k).
    intros i .
    apply in_bar_1, ; trivial.
    .
  Qed.

  Definition minimizer_pred : sig minimizer.
  Proof using Hmin loop.
    destruct (loop ) as (k & & ).
    exists k; split; auto.
    intros; apply ; .
  Defined.

End minimizer_pred.