Library Coq.funind.Recdef
Require
Export
Coq.funind.FunInd
.
Require
Import
PeanoNat
.
Require
Compare_dec
.
Require
Wf_nat
.
Section
Iter
.
Variable
A
:
Type
.
Fixpoint
iter
(
n
:
nat
) :
(
A
->
A
)
->
A
->
A
:=
fun
(
fl
:
A
->
A
) (
def
:
A
) =>
match
n
with
|
O
=>
def
|
S
m
=>
fl
(
iter
m
fl
def
)
end
.
End
Iter
.
Theorem
le_lt_SS
x
y
:
x
<=
y
->
x
<
S
(
S
y
).
Theorem
Splus_lt
x
y
:
y
<
S
(
x
+
y
).
Theorem
SSplus_lt
x
y
:
x
<
S
(
S
(
x
+
y
)).
Inductive
max_type
(
m
n
:
nat
) :
Set
:=
cmt
:
forall
v
,
m
<=
v
->
n
<=
v
->
max_type
m
n
.
Definition
max
m
n
:
max_type
m
n
.
Definition
Acc_intro_generator_function
:=
fun
A
R
=> @
Acc_intro_generator
A
R
100.