proposition: Lemma Series_incr_n (a : nat -> R) (n : nat) : (0 < n)%nat -> ex_series a -> Series a = sum_f_R0 a (pred n) + Series (fun k => a (n + k)%nat).
proof: Proof. move => Hn Ha. apply is_series_unique. rewrite Rplus_comm. apply is_series_decr_n with n. by []. rewrite /plus /opp /= sum_n_Reals. ring_simplify (Series (fun k : nat => a (n+ k)%nat) + sum_f_R0 a (pred n) + - sum_f_R0 a (pred n)). apply Series_correct. by apply ex_series_incr_n. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Lim_seq Rbar Hierarchy