proposition: Lemma CRmorph_series_cv : forall {R1 R2 : ConstructiveReals} (f : @ConstructiveRealsMorphism R1 R2) (un : nat -> CRcarrier R1) (l : CRcarrier R1), series_cv un l -> series_cv (fun n => CRmorph f (un n)) (CRmorph f l).
proof: Proof. intros. apply (CR_cv_eq _ (fun n => CRmorph f (CRsum un n))). - intro n. apply CRmorph_sum. - apply CRmorph_cv, H. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveLimits