Library Coq.Reals.Rcomplete
Require
Import
Rbase
.
Require
Import
Rfunctions
.
Require
Import
Rseries
.
Require
Import
SeqProp
.
Require
Import
Max
.
Open
Local
Scope
R_scope
.
Theorem
R_complete
:
forall
Un
:nat ->
R
,
Cauchy_crit
Un
-> {
l
:R |
Un_cv
Un
l
} .