Library Coq.funind.Recdef
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
SSplus_lt
:
forall
p
p'
:
nat
,
p
<
S
(
S
(
p
+
p'
)).
Theorem
Splus_lt
:
forall
p
p'
:
nat
,
p'
<
S
(
p
+
p'
).
Theorem
le_lt_SS
:
forall
x
y
,
x
<=
y
->
x
<
S
(
S
y
).
Inductive
max_type
(
m
n
:
nat
) :
Set
:=
cmt
:
forall
v
,
m
<=
v
->
n
<=
v
->
max_type
m
n
.
Definition
max
:
forall
m
n
:
nat
,
max_type
m
n
.
Defined
.