# Library rt.util.step_function

Require Import rt.util.tactics rt.util.notation rt.util.induction.

Section StepFunction.

Section Defs.

(* We say that a function f... *)
Variable f: nat nat.

(* ...is a step function iff the following holds. *)
Definition is_step_function :=
t, f (t + 1) f t + 1.

End Defs.

Section Lemmas.

(* Let f be any step function over natural numbers. *)
Variable f: nat nat.
Hypothesis H_step_function: is_step_function f.

(* In this 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:
x_mid, x1 x_mid < x2 f x_mid = y.

End ExistsIntermediateValue.

End Lemmas.

End StepFunction.