Library Coq.Reals.ArithProp
Require
Import
Rbase
.
Require
Import
Rbasic_fun
.
Require
Import
Even
.
Require
Import
Div2
.
Require
Import
ArithRing
.
Local
Open
Scope
Z_scope
.
Local
Open
Scope
R_scope
.
Lemma
minus_neq_O
:
forall
n
i
:
nat
, (
i
<
n
)%
nat
-> (
n
-
i
)%
nat
<>
0%
nat
.
Lemma
le_minusni_n
:
forall
n
i
:
nat
, (
i
<=
n
)%
nat
-> (
n
-
i
<=
n
)%
nat
.
Lemma
lt_minus_O_lt
:
forall
m
n
:
nat
, (
m
<
n
)%
nat
-> (0
<
n
-
m
)%
nat
.
Lemma
even_odd_cor
:
forall
n
:
nat
,
exists
p
:
nat
,
n
=
(2
*
p
)%
nat
\/
n
=
S
(2
*
p
).
Lemma
le_double
:
forall
m
n
:
nat
, (2
*
m
<=
2
*
n
)%
nat
-> (
m
<=
n
)%
nat
.
Here, we have the euclidian division This lemma is used in the proof of sin_eq_0 : (sin x)=0<->x=kPI
Lemma
euclidian_division
:
forall
x
y
:
R
,
y
<>
0 ->
exists
k
:
Z
,
(
exists
r
:
R
,
x
=
IZR
k
*
y
+
r
/\
0
<=
r
<
Rabs
y
)
.
Lemma
tech8
:
forall
n
i
:
nat
, (
n
<=
S
n
+
i
)%
nat
.