Coq translation of a solution to the Valley Problem

P1_valley.v

(* This is a Coq translation of this solution: https://github.com/AndrasKovacs/misc-stuff/blob/master/agda/mathprobs/p01.agda *)
(* to this https://coq-math-problems.github.io/Problem1/ *)
 
Require Import Coq.Arith.Arith.

Definition decr (f : nat -> nat) := forall n, f (S n) <= f n.

Definition n_valley n (f : nat -> nat) i := forall i', i' < n -> f (S (i' + i)) = f (i' + i).

Lemma is_n_valley {f} n : decr f -> forall i, n_valley n f i \/ (exists i', f i' < f i).
Proof.
  induction n; intros Hd i.
  - left; intros i' H. exfalso; exact (Nat.nlt_0_r _ H).
  - destruct (Nat.lt_trichotomy (f (S i)) (f i)) as [Hlt | [Heq | Hgt]].
    + right; eauto.
    + destruct (IHn Hd (S i)) as [Hv | Hex]; [left | right].
      * intros i' Hlt; destruct i'; [trivial |].
        specialize (Hv i' (lt_S_n _ _ Hlt)).
        now rewrite Nat.add_succ_comm.
      * rewrite Heq in Hex; eauto.
    + exfalso; exact ((lt_not_le _ _ Hgt) (Hd i)).
Qed.

(* tactic-based version *)
Lemma p01 {f} n : decr f -> exists i', n_valley n f i'.
Proof.
  intros Hd.
  enough (forall x i, f i = x -> exists i' : nat, n_valley n f i') as H; [now apply (H (f 0) 0) |].
  induction x as [x IH] using lt_wf_ind; intros i Heq.
  destruct (is_n_valley n Hd i) as [| [? ?]]; subst; eauto.
Qed.

(* proof-term-based version *)
Definition p01' {f} n (Hd : decr f) : exists i', n_valley n f i' :=
  lt_wf_ind (f 0)
     (fun x => forall i, f i = x -> exists i', n_valley n f i')
     (fun x IH i Heq =>
        match is_n_valley n Hd i with
        | or_introl H => ex_intro _ i H
        | or_intror (ex_intro _ i' Hlt) =>
            IH (f i') (eq_ind (f i) _ Hlt x Heq) i' eq_refl
        end) 0 eq_refl.