proposition: Lemma series_cv_minus : forall {R : ConstructiveReals} (u v : nat -> CRcarrier R) (s t : CRcarrier R), series_cv u s -> series_cv v t -> series_cv (fun n => u n - v n) (s - t).
proof: Proof. intros. apply (CR_cv_eq _ (fun n => CRsum u n - CRsum v n)). - intro n. symmetry. unfold CRminus. rewrite sum_plus. rewrite sum_opp. reflexivity. - apply CR_cv_plus. + exact H. + apply CR_cv_opp. exact H0. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveLimits