proposition: Lemma series_cv_opp : forall {R : ConstructiveReals} (s : CRcarrier R) (u : nat -> CRcarrier R), series_cv u s -> series_cv (fun n => - u n) (- s).
proof: Proof. intros. intros p. specialize (H p) as [N H]. exists N. intros n H0. setoid_replace (CRsum (fun n0 : nat => - u n0) n - - s) with (-(CRsum (fun n0 : nat => u n0) n - s)). - rewrite CRabs_opp. apply H, H0. - unfold CRminus. rewrite sum_opp. rewrite CRopp_plus_distr. reflexivity. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveLimits