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