proposition: Lemma series_cv_shift' : forall {R : ConstructiveReals} (un : nat -> CRcarrier R) (s : CRcarrier R) (shift : nat), series_cv un s -> series_cv (fun n => un (n+shift)%nat) (s - match shift with | O => 0 | S p => CRsum un p end).
proof: Proof. intros. destruct shift as [|p]. - unfold CRminus. rewrite CRopp_0. rewrite CRplus_0_r. apply (series_cv_eq un). + intros. rewrite Nat.add_0_r. reflexivity. + apply H. - apply (CR_cv_eq _ (fun n => CRsum un (n + S p) - CRsum un p)). + intros. rewrite Nat.add_comm. unfold CRminus. rewrite sum_assoc. simpl. rewrite CRplus_comm, <- CRplus_assoc. rewrite CRplus_opp_l, CRplus_0_l. apply CRsum_eq. intros. rewrite (Nat.add_comm i). reflexivity. + apply CR_cv_plus. * apply (CR_cv_shift' _ (S p) _ H). * intros n. exists (Pos.to_nat n). intros. unfold CRminus. simpl. rewrite CRopp_involutive, CRplus_opp_l. rewrite CRabs_right. -- apply CR_of_Q_le. discriminate. -- apply CRle_refl. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveLimits