Defining a functional that finds a non-decreasing abscissa for any function from nat to nat

non_decr_functional.v

Require Import Lia.

Lemma non_decr_point_aux : forall (n : nat) (f : nat -> nat),
  f 0 <= n -> { x : nat & f x <= f (S x) }.
Proof.
  induction n; intros f f0.
  - exists 0; lia.
  - destruct (Compare_dec.le_lt_dec (f 0) (f 1))
      as [f0_nondecr|f0_decr].
    + exists 0; exact f0_nondecr.
    + pose (g := fun x => f (S x)).
      assert (g 0 <= n) as g0_bound by (unfold g; lia).
      destruct (IHn g g0_bound) as [x gx_nondecr].
      exists (S x); exact gx_nondecr.
Defined.

Definition non_decr_point : forall (f : nat -> nat),
  { x : nat & f x <= f (S x) } :=
  fun f => non_decr_point_aux (f 0) f (le_n (f 0)).