proposition: Lemma series_cv_abs_cv : forall {R : ConstructiveReals} (u : nat -> CRcarrier R) (cau : CR_cauchy R (CRsum (fun n => CRabs R (u n)))), series_cv u (let (l,_):= series_cv_abs u cau in l).
proof: Proof. intros. destruct (series_cv_abs u cau). exact s. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveLimits