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
.
Open
Local
Scope
nat_scope
.
Open
Local
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
.