From mathcomp Require Import ssreflect ssrbool eqtype ssrnat.
Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing]
Require Import prosa.util.tactics prosa.util.notation.

(** 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.

  (** 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 [t] 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
        (* apply DELTA. *) 
        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
      induction delta.
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.

  (** 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
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 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
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 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
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 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 
        -
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.