proposition: Lemma Rcauchy_complete_eq : forall {R : ConstructiveReals} (xn : nat -> CRcarrier R) (cau : CR_cauchy R xn) (a : CRcarrier R), CR_cv R xn a -> (let (l,_) := CR_complete R xn cau in l) == a.
proof: Proof. intros. destruct (CR_complete R xn cau). apply (CR_cv_unique xn); assumption. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete ConstructiveDiagonal ConstructiveUniformCont