``` ```

Specification of : interval

``` Require Export Setoid. Set Implicit Arguments. Set Strict Implicit. ```

Preliminaries

``` ```

`comp`

`comp f n x` is defined as
``` Fixpoint comp (A:Type) (f : A -> A -> A) (x:A) (u : nat -> A) (n:nat) {struct n}: A :=    match n with O => x | S p => f (u p) (comp f x u p) end.        Lemma comp0 : forall (A:Type) (f : A -> A -> A) (x:A) (u : nat -> A),               comp f x u 0 = x. Lemma compS : forall (A:Type) (f : A -> A -> A) (x:A) (u : nat -> A) (n:nat),               comp f x u (S n) = f (u n) (comp f x u n). ```

monotonicity of sequences for an arbitrary relation

``` Definition mon_seq (A:Type) (le : A -> A -> Prop) (f:nat ->A)   := forall n m, (n <= m) -> (le (f n) (f m)). Definition decr_seq (A:Type) (le : A -> A -> Prop) (f:nat ->A)   := forall n m, (n <= m) -> (le (f m) (f n)). ```

Specification of

``` ```
 Constants : and Constructor : `Unth` Operations : , , `inv` Relations : ,
``` Module Type Universe. Parameter U : Type. Bind Scope U_scope with U. Parameters Ueq Ule : U -> U -> Prop. Parameters U0 U1 : U. Parameters Uplus Umult : U -> U -> U. Parameter Uinv : U -> U. Parameter Unth : nat -> U. Infix "+" := Uplus : U_scope. Infix "*" := Umult : U_scope. Infix "==" := Ueq (at level 70) : U_scope. Infix "<=" := Ule : U_scope. Open Scope U_scope. ```

Properties

``` Hypothesis Ueq_refl : forall x:U, x == x. Hypothesis Ueq_sym : forall x y:U, x == y -> y == x. Hypothesis Udiff_0_1 : ~(U0 == U1). Hypothesis Upos : forall x:U, (U0 <= x). Hypothesis Unit : forall x:U, (x <= U1). Hypothesis Uplus_sym : forall x y:U, (x + y) == (y + x). Hypothesis Uplus_assoc : forall x y z:U, (x + (y + z)) == (x + y + z). Hypothesis Uplus_zero_left : forall x:U, (U0 + x) == x. Hypothesis Umult_sym : forall x y:U, (x * y) == (y * x). Hypothesis Umult_assoc : forall x y z:U, (x * (y * z)) == (x * y * z). Hypothesis Umult_one_left : forall x:U, (U1 * x) == x. Hypothesis Uinv_one : (Uinv U1) == U0. Hypothesis Uinv_opp_left : forall x, (Uinv x) + x == U1. ```
 holds when does not overflow
``` Hypothesis Uinv_plus_left      : forall x y, y <= (Uinv x) -> Uinv (x + y) + x == Uinv y. ```
 holds when does not overflow
``` Hypothesis Udistr_plus_right : forall x y z:U,           (x <= Uinv y) -> ((x + y) * z) == (x * z + y * z). ``` ``` Hypothesis Udistr_inv_right :   forall x y:U, Uinv (x * y) == (Uinv x) * y + (Uinv y). ```
 The relation is reflexive, transitive and anti-symmetric
``` Hypothesis Ueq_le : forall x y:U, x == y -> x <= y. Hypothesis Ule_trans   : forall x y z:U, (x <= y) -> (y <= z) -> (x <= z). Hypothesis Ule_antisym   : forall x y:U, (x <= y) -> (y <= x) -> (x == y). ```
 Totality of the order
``` Hypothesis Ueq_double_neg   : forall x y : U, ~~(x == y) -> (x == y). Hypothesis Ule_total   : forall x y : U, (x <= y) \/ (y <= x). ```
 The relation is compatible with operators
``` Hypothesis Uplus_le_compat_right : forall x y z:U, (x <= y) -> (x + z) <= (y + z). Hypothesis Umult_le_compat_right : forall x y z:U, (x <= y) -> (x * z) <= (y * z). Hypothesis Uinv_le_compat   : forall x y:U, x <= y -> Uinv y <= Uinv x. ```
 Properties of simplification in case there is no overflow
``` Hypothesis Uplus_le_simpl_right : forall x y z:U, (z <= (Uinv x)) -> ((x + z) <= (y + z)) -> (x <= y). Hypothesis Umult_le_simpl_left :  forall x y z: U, ~(U0 == z) -> (z * x) <= (z * y) -> x <= y . ```
 `Unth`
``` Hypothesis Unth_prop :    forall n, (Unth n) == Uinv (comp Uplus U0 (fun k => Unth n) n). ```

archimedian

``` Hypothesis archimedian :    forall x, ~x == U0 -> exists n, Unth n <= x. ```

least upper bound, corresponds to limit for increasing sequences

``` Variable lub : (nat -> U) -> U. Hypothesis le_lub : forall (f : nat -> U) (n:nat), (f n) <= (lub f). Hypothesis lub_le : forall (f : nat -> U) (x:U),                            (forall n:nat, f n <= x) -> (lub f) <= x. ```

stability properties of lubs

``` Hypothesis lub_eq_plus_cte_right :    forall (f : nat -> U) (k:U), lub (fun n => (f n) + k) == (lub f) + k. Hypothesis lub_eq_mult : forall k : U, forall f : nat -> U,    lub (fun n => (k * (f n))) == k * lub f. End Universe. ```