Library Coq.Reals.Rtrigo
Require
Import
Rbase
.
Require
Import
Rfunctions
.
Require
Import
SeqSeries
.
Require
Export
Rtrigo_fun
.
Require
Export
Rtrigo_def
.
Require
Export
Rtrigo_alt
.
Require
Export
Cos_rel
.
Require
Export
Cos_plus
.
Require
Import
ZArith_base
.
Require
Import
Zcomplements
.
Require
Import
Classical_Prop
.
Require
Import
Fourier
.
Require
Import
Ranalysis1
.
Require
Import
Rsqrt_def
.
Require
Import
PSeries_reg
.
Require
Export
Rtrigo1
.
Require
Export
Ratan
.
Require
Export
Machin
.