proposition: Lemma series_cv_triangle : forall {R : ConstructiveReals} (u : nat -> CRcarrier R) (s sAbs : CRcarrier R), series_cv u s -> series_cv (fun n => CRabs R (u n)) sAbs -> CRabs R s <= sAbs.
proof: Proof. intros. apply (CR_cv_le (fun n => CRabs R (CRsum u n)) (CRsum (fun n => CRabs R (u n)))). - intros. apply multiTriangleIneg. - apply CR_cv_abs_cont. assumption. - assumption. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveLimits