Library Coq.Reals.Cos_plus
Require
Import
Rbase
.
Require
Import
Rfunctions
.
Require
Import
SeqSeries
.
Require
Import
Rtrigo_def
.
Require
Import
Cos_rel
.
Require
Import
Max
.
Local
Open
Scope
nat_scope
.
Local
Open
Scope
R_scope
.
Definition
Majxy
(
x
y
:
R
) (
n
:
nat
) :
R
:=
Rmax
1 (
Rmax
(
Rabs
x
) (
Rabs
y
))
^
(
4
*
S
n
)
/
INR
(
fact
n
).
Lemma
Majxy_cv_R0
:
forall
x
y
:
R
,
Un_cv
(
Majxy
x
y
) 0.
Lemma
reste1_maj
:
forall
(
x
y
:
R
) (
N
:
nat
),
(0
<
N
)%
nat
->
Rabs
(
Reste1
x
y
N
)
<=
Majxy
x
y
(
pred
N
).
Lemma
reste2_maj
:
forall
(
x
y
:
R
) (
N
:
nat
), (0
<
N
)%
nat
->
Rabs
(
Reste2
x
y
N
)
<=
Majxy
x
y
N
.
Lemma
reste1_cv_R0
:
forall
x
y
:
R
,
Un_cv
(
Reste1
x
y
) 0.
Lemma
reste2_cv_R0
:
forall
x
y
:
R
,
Un_cv
(
Reste2
x
y
) 0.
Lemma
reste_cv_R0
:
forall
x
y
:
R
,
Un_cv
(
Reste
x
y
) 0.
Theorem
cos_plus
:
forall
x
y
:
R
,
cos
(
x
+
y
)
=
cos
x
*
cos
y
-
sin
x
*
sin
y
.