proposition: Lemma series_cv_shift : forall {R : ConstructiveReals} (f : nat -> CRcarrier R) k l, series_cv (fun n => f (S k + n)%nat) l -> series_cv f (l + CRsum f k).
proof: Proof. intros. intro p. specialize (H p) as [n nmaj]. exists (S k+n)%nat. intros. destruct (Nat.le_exists_sub (S k) i). - apply (Nat.le_trans _ (S k + 0)). + rewrite Nat.add_0_r. apply Nat.le_refl. + apply (Nat.le_trans _ (S k + n)). * apply Nat.add_le_mono_l, Nat.le_0_l. * exact H. - destruct H0. subst i. rewrite Nat.add_comm in H. rewrite <- Nat.add_le_mono_r in H. specialize (nmaj x H). unfold CRminus. rewrite Nat.add_comm, (sum_assoc f k x). setoid_replace (CRsum f k + CRsum (fun k0 : nat => f (S k + k0)%nat) x - (l + CRsum f k)) with (CRsum (fun k0 : nat => f (S k + k0)%nat) x - l). + exact nmaj. + unfold CRminus. rewrite (CRplus_comm (CRsum f k)). rewrite CRplus_assoc. apply CRplus_morph. * reflexivity. * rewrite CRplus_comm, CRopp_plus_distr, CRplus_assoc. rewrite CRplus_opp_l, CRplus_0_r. reflexivity. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveLimits