proposition: Lemma series_cv_scale : forall {R : ConstructiveReals} (a : CRcarrier R) (s : CRcarrier R) (u : nat -> CRcarrier R), series_cv u s -> series_cv (fun n => (u n) * a) (s * a).
proof: Proof. intros. apply (CR_cv_eq _ (fun n => CRsum u n * a)). - intro n. rewrite sum_scale. reflexivity. - apply CR_cv_scale, H. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveLimits