Library Coq.Reals.Rcomplete

Require Import Rbase.
Require Import Rfunctions.
Require Import Rseries.
Require Import SeqProp.
Local Open Scope R_scope.


Theorem R_complete :
  forall Un:nat -> R, Cauchy_crit Un -> { l:R | Un_cv Un l } .

Require Import Max.