proposition: Lemma Rcauchy_complete_cv : forall {R : ConstructiveReals } (un : nat -> CRcarrier R) (cau : CR_cauchy R un) (a : CRcarrier R), CR_cv R un a -> ((let (x,_) := CR_complete R un cau in x) == a)%ConstructiveReals.
proof: Proof. intros. destruct (CR_complete R un cau). exact (CR_cv_unique un _ _ c H). Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTFullSets CMTIntegrableSets CMTprofile