From mathcomp Require Import ssreflect ssrbool eqtype ssrnat zify.zify.
[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done]
[Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done]
[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
Serlib plugin: coq-elpi.elpi is not available: serlib support is missing.
Incremental checking for commands in this plugin will be impacted.
[Loading ML file coq-elpi.elpi ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_core_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Require Import prosa.util.tactics prosa.util.notation prosa.util.rel.

(** We say that a function [f] is a unit growth function iff for any
    time instant [t] it holds that [f (t + 1) <= f t + 1]. *)
Definition unit_growth_function (f : nat -> nat) :=
  forall t, f (t + 1) <= f t + 1.

(** In this section, we prove a few useful lemmas about unit growth functions. *)
Section Lemmas.

  (** Let [f] be any unit growth function over natural numbers. *)
  Variable f : nat -> nat.
  Hypothesis H_unit_growth_function : unit_growth_function f.

  (** Since [f] is a unit-growth function, the value of [f] after [k]
      steps is at most [k] greater than its value at the starting
      point. *)
  Lemma unit_growth_function_k_steps_bounded :
    forall (x k : nat),
      f (x + k) <= k + f x.
f: nat -> nat
H_unit_growth_function: unit_growth_function f
forall x k : nat, f (x + k) <= k + f x
  Proof.
f: nat -> nat
H_unit_growth_function: unit_growth_function f
forall x k : nat, f (x + k) <= k + f x
    intros x k; induction k.
f: nat -> nat
H_unit_growth_function: unit_growth_function f
x: nat
f (x + 0) <= 0 + f x
f: nat -> nat
H_unit_growth_function: unit_growth_function f
x, k: nat
IHk: f (x + k) <= k + f x
f (x + k.+1) <= k.+1 + f x
    {
f: nat -> nat
H_unit_growth_function: unit_growth_function f
x: nat
f (x + 0) <= 0 + f x by rewrite addn0 add0n. }
f: nat -> nat
H_unit_growth_function: unit_growth_function f
x, k: nat
IHk: f (x + k) <= k + f x
f (x + k.+1) <= k.+1 + f x
    {
f: nat -> nat
H_unit_growth_function: unit_growth_function f
x, k: nat
IHk: f (x + k) <= k + f x
f (x + k.+1) <= k.+1 + f x rewrite addnS; apply: leq_trans.
f: nat -> nat
H_unit_growth_function: unit_growth_function f
x, k: nat
IHk: f (x + k) <= k + f x
f (x + k).+1 <= ?Goal
f: nat -> nat
H_unit_growth_function: unit_growth_function f
x, k: nat
IHk: f (x + k) <= k + f x
?Goal <= k.+1 + f x
      {
f: nat -> nat
H_unit_growth_function: unit_growth_function f
x, k: nat
IHk: f (x + k) <= k + f x
f (x + k).+1 <= ?Goal by rewrite -addn1; apply H_unit_growth_function. }
f: nat -> nat
H_unit_growth_function: unit_growth_function f
x, k: nat
IHk: f (x + k) <= k + f x
f (x + k) + 1 <= k.+1 + f x
      {
f: nat -> nat
H_unit_growth_function: unit_growth_function f
x, k: nat
IHk: f (x + k) <= k + f x
f (x + k) + 1 <= k.+1 + f x lia. }
    }
  Qed.

  (** In the following section, we prove a result similar to the
      intermediate value theorem for continuous functions. *)
  Section ExistsIntermediateValue.

    (** Consider any interval <<[x1, x2]>>. *)
    Variable x1 x2 : nat.
    Hypothesis H_is_interval : x1 <= x2.

    (** Let [y] be any value such that [f x1 <= y < f x2]. *)
    Variable y : nat.
    Hypothesis H_between : f x1 <= y < f x2.

    (** Then, we prove that there exists an intermediate point [x_mid] such that [f x_mid = y]. *)
    Lemma exists_intermediate_point :
      exists x_mid,
        x1 <= x_mid < x2 /\ f x_mid = y.
f: nat -> nat
H_unit_growth_function: unit_growth_function f
x1, x2: nat
H_is_interval: x1 <= x2
y: nat
H_between: f x1 <= y < f x2
exists x_mid : nat, x1 <= x_mid < x2 /\ f x_mid = y
    Proof.
f: nat -> nat
H_unit_growth_function: unit_growth_function f
x1, x2: nat
H_is_interval: x1 <= x2
y: nat
H_between: f x1 <= y < f x2
exists x_mid : nat, x1 <= x_mid < x2 /\ f x_mid = y
      rename H_is_interval into INT, H_unit_growth_function into UNIT, H_between into BETWEEN.
f: nat -> nat
UNIT: unit_growth_function f
x1, x2: nat
INT: x1 <= x2
y: nat
BETWEEN: f x1 <= y < f x2
exists x_mid : nat, x1 <= x_mid < x2 /\ f x_mid = y
      move: x2 INT BETWEEN; clear x2.
f: nat -> nat
UNIT: unit_growth_function f
x1, y: nat
forall x2 : nat,
x1 <= x2 ->
f x1 <= y < f x2 ->
exists x_mid : nat, x1 <= x_mid < x2 /\ f x_mid = y
      suff DELTA:
        forall delta,
          f x1 <= y < f (x1 + delta) ->
          exists x_mid, x1 <= x_mid < x1 + delta /\ f x_mid = y.
f: nat -> nat
UNIT: unit_growth_function f
x1, y: nat
DELTA: forall delta : nat,
f x1 <= y < f (x1 + delta) ->
exists x_mid : nat,
  x1 <= x_mid < x1 + delta /\ f x_mid = y
forall x2 : nat,
x1 <= x2 ->
f x1 <= y < f x2 ->
exists x_mid : nat, x1 <= x_mid < x2 /\ f x_mid = y
f: nat -> nat
UNIT: unit_growth_function f
x1, y: nat
forall delta : nat,
f x1 <= y < f (x1 + delta) ->
exists x_mid : nat,
  x1 <= x_mid < x1 + delta /\ f x_mid = y
      {
f: nat -> nat
UNIT: unit_growth_function f
x1, y: nat
DELTA: forall delta : nat,
f x1 <= y < f (x1 + delta) ->
exists x_mid : nat,
  x1 <= x_mid < x1 + delta /\ f x_mid = y
forall x2 : nat,
x1 <= x2 ->
f x1 <= y < f x2 ->
exists x_mid : nat, x1 <= x_mid < x2 /\ f x_mid = y move => x2 LE /andP [GEy LTy].
f: nat -> nat
UNIT: unit_growth_function f
x1, y: nat
DELTA: forall delta : nat,
f x1 <= y < f (x1 + delta) ->
exists x_mid : nat,
  x1 <= x_mid < x1 + delta /\ f x_mid = y
x2: nat
LE: x1 <= x2
GEy: f x1 <= y
LTy: y < f x2
exists x_mid : nat, x1 <= x_mid < x2 /\ f x_mid = y
        specialize (DELTA (x2 - x1)); feed DELTA.
f: nat -> nat
UNIT: unit_growth_function f
x1, y, x2: nat
DELTA: f x1 <= y < f (x1 + (x2 - x1)) ->
exists x_mid : nat,
  x1 <= x_mid < x1 + (x2 - x1) /\ f x_mid = y
LE: x1 <= x2
GEy: f x1 <= y
LTy: y < f x2
f x1 <= y < f (x1 + (x2 - x1))
f: nat -> nat
UNIT: unit_growth_function f
x1, y, x2: nat
DELTA: exists x_mid : nat,
  x1 <= x_mid < x1 + (x2 - x1) /\ f x_mid = y
LE: x1 <= x2
GEy: f x1 <= y
LTy: y < f x2
exists x_mid : nat, x1 <= x_mid < x2 /\ f x_mid = y
        {
f: nat -> nat
UNIT: unit_growth_function f
x1, y, x2: nat
DELTA: f x1 <= y < f (x1 + (x2 - x1)) ->
exists x_mid : nat,
  x1 <= x_mid < x1 + (x2 - x1) /\ f x_mid = y
LE: x1 <= x2
GEy: f x1 <= y
LTy: y < f x2
f x1 <= y < f (x1 + (x2 - x1)) by apply/andP; split; last by rewrite addnBA // addKn. }
f: nat -> nat
UNIT: unit_growth_function f
x1, y, x2: nat
DELTA: exists x_mid : nat,
  x1 <= x_mid < x1 + (x2 - x1) /\ f x_mid = y
LE: x1 <= x2
GEy: f x1 <= y
LTy: y < f x2
exists x_mid : nat, x1 <= x_mid < x2 /\ f x_mid = y
        by rewrite subnKC in DELTA.
      }
f: nat -> nat
UNIT: unit_growth_function f
x1, y: nat
forall delta : nat,
f x1 <= y < f (x1 + delta) ->
exists x_mid : nat,
  x1 <= x_mid < x1 + delta /\ f x_mid = y
      elim=> [|delta IHdelta].
f: nat -> nat
UNIT: unit_growth_function f
x1, y: nat
f x1 <= y < f (x1 + 0) ->
exists x_mid : nat,
  x1 <= x_mid < x1 + 0 /\ f x_mid = y
f: nat -> nat
UNIT: unit_growth_function f
x1, y, delta: nat
IHdelta: f x1 <= y < f (x1 + delta) ->
exists x_mid : nat,
  x1 <= x_mid < x1 + delta /\ f x_mid = y
f x1 <= y < f (x1 + delta.+1) ->
exists x_mid : nat,
  x1 <= x_mid < x1 + delta.+1 /\ f x_mid = y
      {
f: nat -> nat
UNIT: unit_growth_function f
x1, y: nat
f x1 <= y < f (x1 + 0) ->
exists x_mid : nat,
  x1 <= x_mid < x1 + 0 /\ f x_mid = y rewrite addn0; move => /andP [GE0 LT0].
f: nat -> nat
UNIT: unit_growth_function f
x1, y: nat
GE0: f x1 <= y
LT0: y < f x1
exists x_mid : nat, x1 <= x_mid < x1 /\ f x_mid = y
        by apply (leq_ltn_trans GE0) in LT0; rewrite ltnn in LT0.
      }
f: nat -> nat
UNIT: unit_growth_function f
x1, y, delta: nat
IHdelta: f x1 <= y < f (x1 + delta) ->
exists x_mid : nat,
  x1 <= x_mid < x1 + delta /\ f x_mid = y
f x1 <= y < f (x1 + delta.+1) ->
exists x_mid : nat,
  x1 <= x_mid < x1 + delta.+1 /\ f x_mid = y
      {
f: nat -> nat
UNIT: unit_growth_function f
x1, y, delta: nat
IHdelta: f x1 <= y < f (x1 + delta) ->
exists x_mid : nat,
  x1 <= x_mid < x1 + delta /\ f x_mid = y
f x1 <= y < f (x1 + delta.+1) ->
exists x_mid : nat,
  x1 <= x_mid < x1 + delta.+1 /\ f x_mid = y move => /andP [GT LT].
f: nat -> nat
UNIT: unit_growth_function f
x1, y, delta: nat
IHdelta: f x1 <= y < f (x1 + delta) ->
exists x_mid : nat,
  x1 <= x_mid < x1 + delta /\ f x_mid = y
GT: f x1 <= y
LT: y < f (x1 + delta.+1)
exists x_mid : nat,
  x1 <= x_mid < x1 + delta.+1 /\ f x_mid = y
        specialize (UNIT (x1 + delta)); rewrite leq_eqVlt in UNIT.
f: nat -> nat
x1, delta, y: nat
IHdelta: f x1 <= y < f (x1 + delta) ->
exists x_mid : nat,
  x1 <= x_mid < x1 + delta /\ f x_mid = y
GT: f x1 <= y
LT: y < f (x1 + delta.+1)
UNIT: (f (x1 + delta + 1) == f (x1 + delta) + 1)
|| (f (x1 + delta + 1) < f (x1 + delta) + 1)
exists x_mid : nat,
  x1 <= x_mid < x1 + delta.+1 /\ f x_mid = y
        have LE: y <= f (x1 + delta).
f: nat -> nat
x1, delta, y: nat
IHdelta: f x1 <= y < f (x1 + delta) ->
exists x_mid : nat,
  x1 <= x_mid < x1 + delta /\ f x_mid = y
GT: f x1 <= y
LT: y < f (x1 + delta.+1)
UNIT: (f (x1 + delta + 1) == f (x1 + delta) + 1)
|| (f (x1 + delta + 1) < f (x1 + delta) + 1)
y <= f (x1 + delta)
f: nat -> nat
x1, delta, y: nat
IHdelta: f x1 <= y < f (x1 + delta) ->
exists x_mid : nat,
  x1 <= x_mid < x1 + delta /\ f x_mid = y
GT: f x1 <= y
LT: y < f (x1 + delta.+1)
UNIT: (f (x1 + delta + 1) == f (x1 + delta) + 1)
|| (f (x1 + delta + 1) < f (x1 + delta) + 1)
LE: y <= f (x1 + delta)
exists x_mid : nat,
  x1 <= x_mid < x1 + delta.+1 /\ f x_mid = y
        {
f: nat -> nat
x1, delta, y: nat
IHdelta: f x1 <= y < f (x1 + delta) ->
exists x_mid : nat,
  x1 <= x_mid < x1 + delta /\ f x_mid = y
GT: f x1 <= y
LT: y < f (x1 + delta.+1)
UNIT: (f (x1 + delta + 1) == f (x1 + delta) + 1)
|| (f (x1 + delta + 1) < f (x1 + delta) + 1)
y <= f (x1 + delta) move: UNIT => /orP [/eqP EQ | UNIT]; first by rewrite !addn1 in EQ; rewrite addnS EQ ltnS in LT.
f: nat -> nat
x1, delta, y: nat
IHdelta: f x1 <= y < f (x1 + delta) ->
exists x_mid : nat,
  x1 <= x_mid < x1 + delta /\ f x_mid = y
GT: f x1 <= y
LT: y < f (x1 + delta.+1)
UNIT: f (x1 + delta + 1) < f (x1 + delta) + 1
y <= f (x1 + delta)
          rewrite [X in _ < X]addn1 ltnS in UNIT.
f: nat -> nat
x1, delta, y: nat
IHdelta: f x1 <= y < f (x1 + delta) ->
exists x_mid : nat,
  x1 <= x_mid < x1 + delta /\ f x_mid = y
GT: f x1 <= y
LT: y < f (x1 + delta.+1)
UNIT: f (x1 + delta + 1) <= f (x1 + delta)
y <= f (x1 + delta)
          apply: (leq_trans _ UNIT).
f: nat -> nat
x1, delta, y: nat
IHdelta: f x1 <= y < f (x1 + delta) ->
exists x_mid : nat,
  x1 <= x_mid < x1 + delta /\ f x_mid = y
GT: f x1 <= y
LT: y < f (x1 + delta.+1)
UNIT: f (x1 + delta + 1) <= f (x1 + delta)
y <= f (x1 + delta + 1)
          by rewrite addn1 -addnS ltnW.
        }
f: nat -> nat
x1, delta, y: nat
IHdelta: f x1 <= y < f (x1 + delta) ->
exists x_mid : nat,
  x1 <= x_mid < x1 + delta /\ f x_mid = y
GT: f x1 <= y
LT: y < f (x1 + delta.+1)
UNIT: (f (x1 + delta + 1) == f (x1 + delta) + 1)
|| (f (x1 + delta + 1) < f (x1 + delta) + 1)
LE: y <= f (x1 + delta)
exists x_mid : nat,
  x1 <= x_mid < x1 + delta.+1 /\ f x_mid = y clear UNIT LT.
f: nat -> nat
x1, delta, y: nat
IHdelta: f x1 <= y < f (x1 + delta) ->
exists x_mid : nat,
  x1 <= x_mid < x1 + delta /\ f x_mid = y
GT: f x1 <= y
LE: y <= f (x1 + delta)
exists x_mid : nat,
  x1 <= x_mid < x1 + delta.+1 /\ f x_mid = y
        rewrite leq_eqVlt in LE.
f: nat -> nat
x1, delta, y: nat
IHdelta: f x1 <= y < f (x1 + delta) ->
exists x_mid : nat,
  x1 <= x_mid < x1 + delta /\ f x_mid = y
GT: f x1 <= y
LE: (y == f (x1 + delta)) || (y < f (x1 + delta))
exists x_mid : nat,
  x1 <= x_mid < x1 + delta.+1 /\ f x_mid = y
        move: LE => /orP [/eqP EQy | LT].
f: nat -> nat
x1, delta, y: nat
IHdelta: f x1 <= y < f (x1 + delta) ->
exists x_mid : nat,
  x1 <= x_mid < x1 + delta /\ f x_mid = y
GT: f x1 <= y
EQy: y = f (x1 + delta)
exists x_mid : nat,
  x1 <= x_mid < x1 + delta.+1 /\ f x_mid = y
f: nat -> nat
x1, delta, y: nat
IHdelta: f x1 <= y < f (x1 + delta) ->
exists x_mid : nat,
  x1 <= x_mid < x1 + delta /\ f x_mid = y
GT: f x1 <= y
LT: y < f (x1 + delta)
exists x_mid : nat,
  x1 <= x_mid < x1 + delta.+1 /\ f x_mid = y
        {
f: nat -> nat
x1, delta, y: nat
IHdelta: f x1 <= y < f (x1 + delta) ->
exists x_mid : nat,
  x1 <= x_mid < x1 + delta /\ f x_mid = y
GT: f x1 <= y
EQy: y = f (x1 + delta)
exists x_mid : nat,
  x1 <= x_mid < x1 + delta.+1 /\ f x_mid = y exists (x1 + delta); split; last by rewrite EQy.
f: nat -> nat
x1, delta, y: nat
IHdelta: f x1 <= y < f (x1 + delta) ->
exists x_mid : nat,
  x1 <= x_mid < x1 + delta /\ f x_mid = y
GT: f x1 <= y
EQy: y = f (x1 + delta)
x1 <= x1 + delta < x1 + delta.+1
          by apply/andP; split; [apply leq_addr | rewrite addnS].
        }
f: nat -> nat
x1, delta, y: nat
IHdelta: f x1 <= y < f (x1 + delta) ->
exists x_mid : nat,
  x1 <= x_mid < x1 + delta /\ f x_mid = y
GT: f x1 <= y
LT: y < f (x1 + delta)
exists x_mid : nat,
  x1 <= x_mid < x1 + delta.+1 /\ f x_mid = y
        {
f: nat -> nat
x1, delta, y: nat
IHdelta: f x1 <= y < f (x1 + delta) ->
exists x_mid : nat,
  x1 <= x_mid < x1 + delta /\ f x_mid = y
GT: f x1 <= y
LT: y < f (x1 + delta)
exists x_mid : nat,
  x1 <= x_mid < x1 + delta.+1 /\ f x_mid = y feed (IHdelta); first by apply/andP; split.
f: nat -> nat
x1, delta, y: nat
IHdelta: exists x_mid : nat,
  x1 <= x_mid < x1 + delta /\ f x_mid = y
GT: f x1 <= y
LT: y < f (x1 + delta)
exists x_mid : nat,
  x1 <= x_mid < x1 + delta.+1 /\ f x_mid = y
          move: IHdelta => [x_mid [/andP [GE0 LT0] EQ0]].
f: nat -> nat
x1, delta, y: nat
GT: f x1 <= y
LT: y < f (x1 + delta)
x_mid: nat
GE0: x1 <= x_mid
LT0: x_mid < x1 + delta
EQ0: f x_mid = y
exists x_mid : nat,
  x1 <= x_mid < x1 + delta.+1 /\ f x_mid = y
          exists x_mid; split; last by done.
f: nat -> nat
x1, delta, y: nat
GT: f x1 <= y
LT: y < f (x1 + delta)
x_mid: nat
GE0: x1 <= x_mid
LT0: x_mid < x1 + delta
EQ0: f x_mid = y
x1 <= x_mid < x1 + delta.+1
          apply/andP; split; first by done.
f: nat -> nat
x1, delta, y: nat
GT: f x1 <= y
LT: y < f (x1 + delta)
x_mid: nat
GE0: x1 <= x_mid
LT0: x_mid < x1 + delta
EQ0: f x_mid = y
x_mid < x1 + delta.+1
          by apply: (leq_trans LT0); rewrite addnS.
        }
      }
    Qed.

  End ExistsIntermediateValue.

  (** Next, we prove the same lemma with slightly different boundary conditions. *)
  Section ExistsIntermediateValueLEQ.

    (** Consider any interval <<[x1, x2]>>. *)
    Variable x1 x2 : nat.
    Hypothesis H_is_interval : x1 <= x2.

    (** Let [y] be any value such that [f x1 <= y <= f x2]. Note that
        [y] is allowed to be equal to [f x2]. *)
    Variable y : nat.
    Hypothesis H_between : f x1 <= y <= f x2.

    (** Then, we prove that there exists an intermediate point [x_mid] such that [f x_mid = y]. *)
    Corollary exists_intermediate_point_leq :
      exists x_mid,
        x1 <= x_mid <= x2 /\ f x_mid = y.
f: nat -> nat
H_unit_growth_function: unit_growth_function f
x1, x2: nat
H_is_interval: x1 <= x2
y: nat
H_between: f x1 <= y <= f x2
exists x_mid : nat, x1 <= x_mid <= x2 /\ f x_mid = y
    Proof.
f: nat -> nat
H_unit_growth_function: unit_growth_function f
x1, x2: nat
H_is_interval: x1 <= x2
y: nat
H_between: f x1 <= y <= f x2
exists x_mid : nat, x1 <= x_mid <= x2 /\ f x_mid = y
      move: (H_between) => /andP [H1 H2].
f: nat -> nat
H_unit_growth_function: unit_growth_function f
x1, x2: nat
H_is_interval: x1 <= x2
y: nat
H_between: f x1 <= y <= f x2
H1: f x1 <= y
H2: y <= f x2
exists x_mid : nat, x1 <= x_mid <= x2 /\ f x_mid = y
      move: H2; rewrite leq_eqVlt => /orP [/eqP EQ | LT].
f: nat -> nat
H_unit_growth_function: unit_growth_function f
x1, x2: nat
H_is_interval: x1 <= x2
y: nat
H_between: f x1 <= y <= f x2
H1: f x1 <= y
EQ: y = f x2
exists x_mid : nat, x1 <= x_mid <= x2 /\ f x_mid = y
f: nat -> nat
H_unit_growth_function: unit_growth_function f
x1, x2: nat
H_is_interval: x1 <= x2
y: nat
H_between: f x1 <= y <= f x2
H1: f x1 <= y
LT: y < f x2
exists x_mid : nat, x1 <= x_mid <= x2 /\ f x_mid = y
      {
f: nat -> nat
H_unit_growth_function: unit_growth_function f
x1, x2: nat
H_is_interval: x1 <= x2
y: nat
H_between: f x1 <= y <= f x2
H1: f x1 <= y
EQ: y = f x2
exists x_mid : nat, x1 <= x_mid <= x2 /\ f x_mid = y exists x2; split.
f: nat -> nat
H_unit_growth_function: unit_growth_function f
x1, x2: nat
H_is_interval: x1 <= x2
y: nat
H_between: f x1 <= y <= f x2
H1: f x1 <= y
EQ: y = f x2
x1 <= x2 <= x2
f: nat -> nat
H_unit_growth_function: unit_growth_function f
x1, x2: nat
H_is_interval: x1 <= x2
y: nat
H_between: f x1 <= y <= f x2
H1: f x1 <= y
EQ: y = f x2
f x2 = y
        -
f: nat -> nat
H_unit_growth_function: unit_growth_function f
x1, x2: nat
H_is_interval: x1 <= x2
y: nat
H_between: f x1 <= y <= f x2
H1: f x1 <= y
EQ: y = f x2
x1 <= x2 <= x2 by apply /andP; split => //.
        -
f: nat -> nat
H_unit_growth_function: unit_growth_function f
x1, x2: nat
H_is_interval: x1 <= x2
y: nat
H_between: f x1 <= y <= f x2
H1: f x1 <= y
EQ: y = f x2
f x2 = y by done.
      }
f: nat -> nat
H_unit_growth_function: unit_growth_function f
x1, x2: nat
H_is_interval: x1 <= x2
y: nat
H_between: f x1 <= y <= f x2
H1: f x1 <= y
LT: y < f x2
exists x_mid : nat, x1 <= x_mid <= x2 /\ f x_mid = y
      {
f: nat -> nat
H_unit_growth_function: unit_growth_function f
x1, x2: nat
H_is_interval: x1 <= x2
y: nat
H_between: f x1 <= y <= f x2
H1: f x1 <= y
LT: y < f x2
exists x_mid : nat, x1 <= x_mid <= x2 /\ f x_mid = y edestruct exists_intermediate_point with (x1 := x1) (x2 := x2) as [mid [NEQ EQ]] => //.
f: nat -> nat
H_unit_growth_function: unit_growth_function f
x1, x2: nat
H_is_interval: x1 <= x2
y: nat
H_between: f x1 <= y <= f x2
H1: f x1 <= y
LT: y < f x2
f x1 <= ?y < f x2
f: nat -> nat
H_unit_growth_function: unit_growth_function f
x1, x2: nat
H_is_interval: x1 <= x2
y: nat
H_between: f x1 <= y <= f x2
H1: f x1 <= y
LT: y < f x2
mid: nat
NEQ: x1 <= mid < x2
EQ: f mid = ?y
exists x_mid : nat, x1 <= x_mid <= x2 /\ f x_mid = y
        {
f: nat -> nat
H_unit_growth_function: unit_growth_function f
x1, x2: nat
H_is_interval: x1 <= x2
y: nat
H_between: f x1 <= y <= f x2
H1: f x1 <= y
LT: y < f x2
f x1 <= ?y < f x2 by apply/andP; split; [ apply H1 | apply LT]. }
f: nat -> nat
H_unit_growth_function: unit_growth_function f
x1, x2: nat
H_is_interval: x1 <= x2
y: nat
H_between: f x1 <= y <= f x2
H1: f x1 <= y
LT: y < f x2
mid: nat
NEQ: x1 <= mid < x2
EQ: f mid = y
exists x_mid : nat, x1 <= x_mid <= x2 /\ f x_mid = y
        exists mid; split; last by done.
f: nat -> nat
H_unit_growth_function: unit_growth_function f
x1, x2: nat
H_is_interval: x1 <= x2
y: nat
H_between: f x1 <= y <= f x2
H1: f x1 <= y
LT: y < f x2
mid: nat
NEQ: x1 <= mid < x2
EQ: f mid = y
x1 <= mid <= x2
        move: NEQ => /andP [NEQ1 NEQ2].
f: nat -> nat
H_unit_growth_function: unit_growth_function f
x1, x2: nat
H_is_interval: x1 <= x2
y: nat
H_between: f x1 <= y <= f x2
H1: f x1 <= y
LT: y < f x2
mid: nat
EQ: f mid = y
NEQ1: x1 <= mid
NEQ2: mid < x2
x1 <= mid <= x2
        by apply/andP; split => //.
      }
    Qed.

  End ExistsIntermediateValueLEQ.

  (** In this section, we, again, prove an analogue of the
      intermediate value theorem, but for predicates over natural
      numbers. *)
  Section ExistsIntermediateValuePredicates.

    (** Let [P] be any predicate on natural numbers. *)
    Variable P : nat -> bool.

    (** Consider a time interval <<[t1,t2]>> such that ... *)
    Variables t1 t2 : nat.
    Hypothesis H_t1_le_t2 : t1 <= t2.

    (** ... [P] doesn't hold for [t1] ... *)
    Hypothesis H_not_P_at_t1 : ~~ P t1.

    (** ... but holds for [t2]. *)
    Hypothesis H_P_at_t2 : P t2.

    (** Then we prove that within time interval <<[t1,t2]>> there exists
        time instant [t] such that [t] is the first time instant when
        [P] holds. *)
    Lemma exists_first_intermediate_point :
      exists t, (t1 < t <= t2) /\ (forall x, t1 <= x < t -> ~~ P x) /\ P t.
f: nat -> nat
H_unit_growth_function: unit_growth_function f
P: nat -> bool
t1, t2: nat
H_t1_le_t2: t1 <= t2
H_not_P_at_t1: ~~ P t1
H_P_at_t2: P t2
exists t : nat,
  t1 < t <= t2 /\
  (forall x : nat, t1 <= x < t -> ~~ P x) /\ P t
    Proof.
f: nat -> nat
H_unit_growth_function: unit_growth_function f
P: nat -> bool
t1, t2: nat
H_t1_le_t2: t1 <= t2
H_not_P_at_t1: ~~ P t1
H_P_at_t2: P t2
exists t : nat,
  t1 < t <= t2 /\
  (forall x : nat, t1 <= x < t -> ~~ P x) /\ P t
      have EX: exists x, P x && (t1 < x <= t2).
f: nat -> nat
H_unit_growth_function: unit_growth_function f
P: nat -> bool
t1, t2: nat
H_t1_le_t2: t1 <= t2
H_not_P_at_t1: ~~ P t1
H_P_at_t2: P t2
exists x : nat, [&& P x, t1 < x & x <= t2]
f: nat -> nat
H_unit_growth_function: unit_growth_function f
P: nat -> bool
t1, t2: nat
H_t1_le_t2: t1 <= t2
H_not_P_at_t1: ~~ P t1
H_P_at_t2: P t2
EX: exists x : nat, [&& P x, t1 < x & x <= t2]
exists t : nat,
  t1 < t <= t2 /\
  (forall x : nat, t1 <= x < t -> ~~ P x) /\ P t
      {
f: nat -> nat
H_unit_growth_function: unit_growth_function f
P: nat -> bool
t1, t2: nat
H_t1_le_t2: t1 <= t2
H_not_P_at_t1: ~~ P t1
H_P_at_t2: P t2
exists x : nat, [&& P x, t1 < x & x <= t2] exists t2.
f: nat -> nat
H_unit_growth_function: unit_growth_function f
P: nat -> bool
t1, t2: nat
H_t1_le_t2: t1 <= t2
H_not_P_at_t1: ~~ P t1
H_P_at_t2: P t2
[&& P t2, t1 < t2 & t2 <= t2]
        apply/andP; split; first by done.
f: nat -> nat
H_unit_growth_function: unit_growth_function f
P: nat -> bool
t1, t2: nat
H_t1_le_t2: t1 <= t2
H_not_P_at_t1: ~~ P t1
H_P_at_t2: P t2
t1 < t2 <= t2
        apply/andP; split; last by done.
f: nat -> nat
H_unit_growth_function: unit_growth_function f
P: nat -> bool
t1, t2: nat
H_t1_le_t2: t1 <= t2
H_not_P_at_t1: ~~ P t1
H_P_at_t2: P t2
t1 < t2
        move: H_t1_le_t2; rewrite leq_eqVlt; move => /orP [/eqP EQ | NEQ1]; last by done.
f: nat -> nat
H_unit_growth_function: unit_growth_function f
P: nat -> bool
t1, t2: nat
H_t1_le_t2: t1 <= t2
H_not_P_at_t1: ~~ P t1
H_P_at_t2: P t2
EQ: t1 = t2
t1 < t2
        by exfalso; subst t2; move: H_not_P_at_t1 => /negP NPt1.
      }
f: nat -> nat
H_unit_growth_function: unit_growth_function f
P: nat -> bool
t1, t2: nat
H_t1_le_t2: t1 <= t2
H_not_P_at_t1: ~~ P t1
H_P_at_t2: P t2
EX: exists x : nat, [&& P x, t1 < x & x <= t2]
exists t : nat,
  t1 < t <= t2 /\
  (forall x : nat, t1 <= x < t -> ~~ P x) /\ P t
      have MIN := ex_minnP EX.
f: nat -> nat
H_unit_growth_function: unit_growth_function f
P: nat -> bool
t1, t2: nat
H_t1_le_t2: t1 <= t2
H_not_P_at_t1: ~~ P t1
H_P_at_t2: P t2
EX: exists x : nat, [&& P x, t1 < x & x <= t2]
MIN: ex_minn_spec
  (fun x : nat => [&& P x, t1 < x & x <= t2])
  (ex_minn
     (P:=fun x : nat =>
         [&& P x, t1 < x & x <= t2]) EX)
exists t : nat,
  t1 < t <= t2 /\
  (forall x : nat, t1 <= x < t -> ~~ P x) /\ P t
      move: MIN => [x /andP [Px /andP [LT1 LT2]] MIN]; clear EX.
f: nat -> nat
H_unit_growth_function: unit_growth_function f
P: nat -> bool
t1, t2: nat
H_t1_le_t2: t1 <= t2
H_not_P_at_t1: ~~ P t1
H_P_at_t2: P t2
x: nat
Px: P x
LT1: t1 < x
LT2: x <= t2
MIN: forall n : nat,
[&& P n, t1 < n & n <= t2] -> x <= n
exists t : nat,
  t1 < t <= t2 /\
  (forall x : nat, t1 <= x < t -> ~~ P x) /\ P t
      exists x; repeat split; [ apply/andP; split | | ]; try done.
f: nat -> nat
H_unit_growth_function: unit_growth_function f
P: nat -> bool
t1, t2: nat
H_t1_le_t2: t1 <= t2
H_not_P_at_t1: ~~ P t1
H_P_at_t2: P t2
x: nat
Px: P x
LT1: t1 < x
LT2: x <= t2
MIN: forall n : nat,
[&& P n, t1 < n & n <= t2] -> x <= n
forall x0 : nat, t1 <= x0 < x -> ~~ P x0
      move => y /andP [NEQ1 NEQ2]; apply/negPn; intros Py.
f: nat -> nat
H_unit_growth_function: unit_growth_function f
P: nat -> bool
t1, t2: nat
H_t1_le_t2: t1 <= t2
H_not_P_at_t1: ~~ P t1
H_P_at_t2: P t2
x: nat
Px: P x
LT1: t1 < x
LT2: x <= t2
MIN: forall n : nat,
[&& P n, t1 < n & n <= t2] -> x <= n
y: nat
NEQ1: t1 <= y
NEQ2: y < x
Py: P y
False
      feed (MIN y).
f: nat -> nat
H_unit_growth_function: unit_growth_function f
P: nat -> bool
t1, t2: nat
H_t1_le_t2: t1 <= t2
H_not_P_at_t1: ~~ P t1
H_P_at_t2: P t2
x: nat
Px: P x
LT1: t1 < x
LT2: x <= t2
MIN: forall n : nat,
[&& P n, t1 < n & n <= t2] -> x <= n
y: nat
NEQ1: t1 <= y
NEQ2: y < x
Py: P y
[&& P y, t1 < y & y <= t2]
f: nat -> nat
H_unit_growth_function: unit_growth_function f
P: nat -> bool
t1, t2: nat
H_t1_le_t2: t1 <= t2
H_not_P_at_t1: ~~ P t1
H_P_at_t2: P t2
x: nat
Px: P x
LT1: t1 < x
LT2: x <= t2
y: nat
MIN: x <= y
NEQ1: t1 <= y
NEQ2: y < x
Py: P y
False
      {
f: nat -> nat
H_unit_growth_function: unit_growth_function f
P: nat -> bool
t1, t2: nat
H_t1_le_t2: t1 <= t2
H_not_P_at_t1: ~~ P t1
H_P_at_t2: P t2
x: nat
Px: P x
LT1: t1 < x
LT2: x <= t2
MIN: forall n : nat,
[&& P n, t1 < n & n <= t2] -> x <= n
y: nat
NEQ1: t1 <= y
NEQ2: y < x
Py: P y
[&& P y, t1 < y & y <= t2] apply/andP; split; first by done.
f: nat -> nat
H_unit_growth_function: unit_growth_function f
P: nat -> bool
t1, t2: nat
H_t1_le_t2: t1 <= t2
H_not_P_at_t1: ~~ P t1
H_P_at_t2: P t2
x: nat
Px: P x
LT1: t1 < x
LT2: x <= t2
MIN: forall n : nat,
[&& P n, t1 < n & n <= t2] -> x <= n
y: nat
NEQ1: t1 <= y
NEQ2: y < x
Py: P y
t1 < y <= t2
        apply/andP; split.
f: nat -> nat
H_unit_growth_function: unit_growth_function f
P: nat -> bool
t1, t2: nat
H_t1_le_t2: t1 <= t2
H_not_P_at_t1: ~~ P t1
H_P_at_t2: P t2
x: nat
Px: P x
LT1: t1 < x
LT2: x <= t2
MIN: forall n : nat,
[&& P n, t1 < n & n <= t2] -> x <= n
y: nat
NEQ1: t1 <= y
NEQ2: y < x
Py: P y
t1 < y
f: nat -> nat
H_unit_growth_function: unit_growth_function f
P: nat -> bool
t1, t2: nat
H_t1_le_t2: t1 <= t2
H_not_P_at_t1: ~~ P t1
H_P_at_t2: P t2
x: nat
Px: P x
LT1: t1 < x
LT2: x <= t2
MIN: forall n : nat,
[&& P n, t1 < n & n <= t2] -> x <= n
y: nat
NEQ1: t1 <= y
NEQ2: y < x
Py: P y
y <= t2
        -
f: nat -> nat
H_unit_growth_function: unit_growth_function f
P: nat -> bool
t1, t2: nat
H_t1_le_t2: t1 <= t2
H_not_P_at_t1: ~~ P t1
H_P_at_t2: P t2
x: nat
Px: P x
LT1: t1 < x
LT2: x <= t2
MIN: forall n : nat,
[&& P n, t1 < n & n <= t2] -> x <= n
y: nat
NEQ1: t1 <= y
NEQ2: y < x
Py: P y
t1 < y move: NEQ1.
f: nat -> nat
H_unit_growth_function: unit_growth_function f
P: nat -> bool
t1, t2: nat
H_t1_le_t2: t1 <= t2
H_not_P_at_t1: ~~ P t1
H_P_at_t2: P t2
x: nat
Px: P x
LT1: t1 < x
LT2: x <= t2
MIN: forall n : nat,
[&& P n, t1 < n & n <= t2] -> x <= n
y: nat
NEQ2: y < x
Py: P y
t1 <= y -> t1 < y rewrite leq_eqVlt; move => /orP [/eqP EQ | NEQ1]; last by done.
f: nat -> nat
H_unit_growth_function: unit_growth_function f
P: nat -> bool
t1, t2: nat
H_t1_le_t2: t1 <= t2
H_not_P_at_t1: ~~ P t1
H_P_at_t2: P t2
x: nat
Px: P x
LT1: t1 < x
LT2: x <= t2
MIN: forall n : nat,
[&& P n, t1 < n & n <= t2] -> x <= n
y: nat
NEQ2: y < x
Py: P y
EQ: t1 = y
t1 < y
          by exfalso; subst y; move: H_not_P_at_t1 => /negP NPt1.
        -
f: nat -> nat
H_unit_growth_function: unit_growth_function f
P: nat -> bool
t1, t2: nat
H_t1_le_t2: t1 <= t2
H_not_P_at_t1: ~~ P t1
H_P_at_t2: P t2
x: nat
Px: P x
LT1: t1 < x
LT2: x <= t2
MIN: forall n : nat,
[&& P n, t1 < n & n <= t2] -> x <= n
y: nat
NEQ1: t1 <= y
NEQ2: y < x
Py: P y
y <= t2 by apply ltnW, leq_trans with x.
      }
f: nat -> nat
H_unit_growth_function: unit_growth_function f
P: nat -> bool
t1, t2: nat
H_t1_le_t2: t1 <= t2
H_not_P_at_t1: ~~ P t1
H_P_at_t2: P t2
x: nat
Px: P x
LT1: t1 < x
LT2: x <= t2
y: nat
MIN: x <= y
NEQ1: t1 <= y
NEQ2: y < x
Py: P y
False
      by move: NEQ2; rewrite ltnNge; move => /negP NEQ2.
    Qed.

  End ExistsIntermediateValuePredicates.

End Lemmas.


(** * Slowing Functions to Unit-Step Growth

    Next, we define and prove a few properties about a function that
    converts any function into a unit-step function. This construction
    will be used later to define Supply-Bound Functions (SBFs), which
    must satisfy this growth constraint in some of the RTAs.  *)

(** ** Slowed Function

    Given a function [F : nat -> nat], we define a slowed version [slowed
    F] such that [slowed F n] grows no faster than one unit per input
    increment. Intuitively, [slowed F] matches [F] when [slowed F n =
    F n], and otherwise "lags behind" [F] to enforce the unit-growth
    constraint.

    The definition is recursive: [slowed F n] is the minimum of [F n]
    and [1 + slowed F (n-1)].  *)
Fixpoint slowed (F : nat -> nat) (n : nat) : nat :=
  match n with
  | 0 => F 0
  | n'.+1 => minn (F n'.+1) (slowed F n').+1
  end.

(** Given two functions [f] and [F], if [f] is a unit-growth function
    and [f <= F] pointwise up to [Δ], then [f Δ <= slowed F Δ]. *)
Lemma slowed_respects_pointwise_leq :
  forall (f F : nat -> nat) (Δ : nat),
    unit_growth_function f  ->
    (forall x, x <= Δ -> f x <= F x) ->
    f Δ <= slowed F Δ.
forall (f F : nat -> nat) (Δ : nat),
unit_growth_function f ->
(forall x : nat, x <= Δ -> f x <= F x) ->
f Δ <= slowed F Δ
Proof.
forall (f F : nat -> nat) (Δ : nat),
unit_growth_function f ->
(forall x : nat, x <= Δ -> f x <= F x) ->
f Δ <= slowed F Δ
  move => f F x SL LE; induction x as [|n IH]; first by apply: LE.
f, F: nat -> nat
n: nat
SL: unit_growth_function f
LE: forall x : nat, x <= n.+1 -> f x <= F x
IH: (forall x : nat, x <= n -> f x <= F x) ->
f n <= slowed F n
f n.+1 <= slowed F n.+1
  have [CLE|Hcase] := leqP (F n.+1) (slowed F n + 1).
f, F: nat -> nat
n: nat
SL: unit_growth_function f
LE: forall x : nat, x <= n.+1 -> f x <= F x
IH: (forall x : nat, x <= n -> f x <= F x) ->
f n <= slowed F n
CLE: F n.+1 <= slowed F n + 1
f n.+1 <= slowed F n.+1
f, F: nat -> nat
n: nat
SL: unit_growth_function f
LE: forall x : nat, x <= n.+1 -> f x <= F x
IH: (forall x : nat, x <= n -> f x <= F x) ->
f n <= slowed F n
Hcase: slowed F n + 1 < F n.+1
f n.+1 <= slowed F n.+1
  {
f, F: nat -> nat
n: nat
SL: unit_growth_function f
LE: forall x : nat, x <= n.+1 -> f x <= F x
IH: (forall x : nat, x <= n -> f x <= F x) ->
f n <= slowed F n
CLE: F n.+1 <= slowed F n + 1
f n.+1 <= slowed F n.+1 rewrite leq_min; apply/andP; split; first by apply LE.
f, F: nat -> nat
n: nat
SL: unit_growth_function f
LE: forall x : nat, x <= n.+1 -> f x <= F x
IH: (forall x : nat, x <= n -> f x <= F x) ->
f n <= slowed F n
CLE: F n.+1 <= slowed F n + 1
f n.+1 <=
((fix slowed (F : nat -> nat) (n : nat) {struct n} :
      nat :=
    match n with
    | 0 => F 0
    | n'.+1 => minn (F n'.+1) (slowed F n').+1
    end) F n).+1
    apply: leq_trans; first by apply LE.
f, F: nat -> nat
n: nat
SL: unit_growth_function f
LE: forall x : nat, x <= n.+1 -> f x <= F x
IH: (forall x : nat, x <= n -> f x <= F x) ->
f n <= slowed F n
CLE: F n.+1 <= slowed F n + 1
F n.+1 <=
((fix slowed (F : nat -> nat) (n : nat) {struct n} :
      nat :=
    match n with
    | 0 => F 0
    | n'.+1 => minn (F n'.+1) (slowed F n').+1
    end) F n).+1
    by rewrite addn1 in CLE.
  }
f, F: nat -> nat
n: nat
SL: unit_growth_function f
LE: forall x : nat, x <= n.+1 -> f x <= F x
IH: (forall x : nat, x <= n -> f x <= F x) ->
f n <= slowed F n
Hcase: slowed F n + 1 < F n.+1
f n.+1 <= slowed F n.+1
  {
f, F: nat -> nat
n: nat
SL: unit_growth_function f
LE: forall x : nat, x <= n.+1 -> f x <= F x
IH: (forall x : nat, x <= n -> f x <= F x) ->
f n <= slowed F n
Hcase: slowed F n + 1 < F n.+1
f n.+1 <= slowed F n.+1 rewrite leq_min; apply/andP; split; first by apply LE.
f, F: nat -> nat
n: nat
SL: unit_growth_function f
LE: forall x : nat, x <= n.+1 -> f x <= F x
IH: (forall x : nat, x <= n -> f x <= F x) ->
f n <= slowed F n
Hcase: slowed F n + 1 < F n.+1
f n.+1 <=
((fix slowed (F : nat -> nat) (n : nat) {struct n} :
      nat :=
    match n with
    | 0 => F 0
    | n'.+1 => minn (F n'.+1) (slowed F n').+1
    end) F n).+1
    apply: leq_trans; first by rewrite -addn1; apply SL.
f, F: nat -> nat
n: nat
SL: unit_growth_function f
LE: forall x : nat, x <= n.+1 -> f x <= F x
IH: (forall x : nat, x <= n -> f x <= F x) ->
f n <= slowed F n
Hcase: slowed F n + 1 < F n.+1
f n + 1 <=
((fix slowed (F : nat -> nat) (n : nat) {struct n} :
      nat :=
    match n with
    | 0 => F 0
    | n'.+1 => minn (F n'.+1) (slowed F n').+1
    end) F n).+1
    by rewrite -[in leqRHS]addn1 leq_add2r; apply IH.
  }
Qed.

(** The [slowed] function grows at most by 1 per step (i.e., it's unit-growth). *)
Lemma slowed_is_unit_step :
  forall (f : nat -> nat),
    unit_growth_function (slowed f).
forall f : nat -> nat, unit_growth_function (slowed f)
Proof.
forall f : nat -> nat, unit_growth_function (slowed f)
  unfold unit_growth_function; intros f x; rewrite !addn1.
f: nat -> nat
x: nat
slowed f x.+1 <= (slowed f x).+1
  by induction x; simpl; lia.
Qed.

(** If [f] is monotone, then [slowed f] is also monotone. *)
Lemma slowed_respects_monotone :
  forall (f : nat -> nat),
    monotone leq f ->
    monotone leq (slowed f).
forall f : nat -> nat,
monotone leq f -> monotone leq (slowed f)
Proof.
forall f : nat -> nat,
monotone leq f -> monotone leq (slowed f)
  move => f MON x y NEQ.
f: nat -> nat
MON: monotone leq f
x, y: nat
NEQ: x <= y
slowed f x <= slowed f y
  interval_to_duration x y k; induction k as [ | k IHk].
f: nat -> nat
MON: monotone leq f
x: nat
slowed f x <= slowed f (x + 0)
f: nat -> nat
MON: monotone leq f
x, k: nat
IHk: slowed f x <= slowed f (x + k)
slowed f x <= slowed f (x + k.+1)
  {
f: nat -> nat
MON: monotone leq f
x: nat
slowed f x <= slowed f (x + 0) by rewrite addn0. }
f: nat -> nat
MON: monotone leq f
x, k: nat
IHk: slowed f x <= slowed f (x + k)
slowed f x <= slowed f (x + k.+1)
  {
f: nat -> nat
MON: monotone leq f
x, k: nat
IHk: slowed f x <= slowed f (x + k)
slowed f x <= slowed f (x + k.+1) rewrite addnS //=; apply:leq_trans; first by apply IHk.
f: nat -> nat
MON: monotone leq f
x, k: nat
IHk: slowed f x <= slowed f (x + k)
slowed f (x + k) <=
minn (f (x + k).+1) (slowed f (x + k)).+1
    move: (MON (x + k) (x + k).+1 ltac:(done)) => MONS.
f: nat -> nat
MON: monotone leq f
x, k: nat
IHk: slowed f x <= slowed f (x + k)
MONS: f (x + k) <= f (x + k).+1
slowed f (x + k) <=
minn (f (x + k).+1) (slowed f (x + k)).+1
    rewrite leq_min; apply/andP; split; last by done.
f: nat -> nat
MON: monotone leq f
x, k: nat
IHk: slowed f x <= slowed f (x + k)
MONS: f (x + k) <= f (x + k).+1
slowed f (x + k) <= f (x + k).+1
    apply: leq_trans; last by apply MONS.
f: nat -> nat
MON: monotone leq f
x, k: nat
IHk: slowed f x <= slowed f (x + k)
MONS: f (x + k) <= f (x + k).+1
slowed f (x + k) <= f (x + k)
    by clear; induction (x + k); [done | simpl; lia].
  }
Qed.