A simple proof that monotone functions over the naturals are cofinal

monotone_cofinal.v

Require Import Lia PeanoNat.

Definition monotone(f : nat -> nat) :=
  forall x, f x < f (S x).

Definition cofinal(f : nat -> nat) :=
  forall x, { y : nat & x < f y }.

Lemma monotone_cofinal : forall f, monotone f -> cofinal f.
Proof.
  intros f f_mon x.
  induction x.
  - destruct (f 0) eqn:f0.
    + destruct (f 1) eqn:f1.
      * absurd (f 0 < f 1).
        ** lia.
        ** apply f_mon.
      * exists 1.
        lia.
    + exists 0.
      lia.
  - destruct IHx as [y fy].
    destruct (Nat.eq_dec (S x) (f y)).
    + exists (S y).
      rewrite e.
      apply f_mon.
    + exists y.
      lia.
Defined.