``` ```

# Study of the class of monotonic functions (Lemma 1.7 and 1.8)

``` Require Export Settings. Section Global.   Variable A: Type.   Section A.     Variables X Y: Type.     Variable TX: reduction_t A X.     Variable TY: reduction_t A Y.     Section A'.       Variable R: relation2 X Y.       Variable E: relation2 X X.       Variable T: relation2 Y Y. ```
identity is monotonic
```       Lemma identity_mon: monotonic TX TY (identity (X:=X) (Y:=Y)). ```
constant-to-simulation is monotonic
```       Lemma constant_mon: simulation TX TY R -> monotonic TX TY (constant R). ```
simulation-right-chaining is monotonic
```       Lemma chaining_r_mon: simulation TY TY T -> monotonic TX TY (chaining_r T). ```
expansion-left-chaining is monotonic
```       Lemma chaining_l_mon: expansion1 TX TX E -> monotonic TX TY (chaining_l E).     End A'.     Variables F G: function X Y.     Hypothesis HF: monotonic TX TY F.     Hypothesis HG: monotonic TX TY G. ```
Composition respect monotonicity
```     Lemma Comp_mon: monotonic TX TY (Comp G F). ```
Binary union respect monotonicity
```     Lemma Union2_mon: monotonic TX TY (Union2 F G).     Section Union.       Variable I: Type.       Variable H: I -> function X Y.       Hypothesis HH: forall i, monotonic TX TY (H i). ```
Union respect monotonicity
```       Lemma Union_mon: monotonic TX TY (Union H).     End Union.   End A.   Section B.     Variables X Y: Type.     Variable TX: reduction_t A X.     Variable TY: reduction_t A Y.     Variables F G: function X Y.     Hypothesis HF: monotonic TX TY F.     Hypothesis HG: monotonic TX TY G. ```
Iteration respect monotonicity
```     Lemma UExp_mon: forall n, monotonic TX TY (fun R => UExp F R n).     Lemma UIter_mon: monotonic TX TY (UIter F).   End B. End Global. ```