proposition: Lemma Series_incr_n_aux (a : nat -> R) (n : nat) : (forall k, (k < n)%nat -> a k = 0) -> Series a = Series (fun k => a (n + k)%nat).
proof: Proof. elim: n => [ | n IH] Ha. by apply Series_ext => k. rewrite IH. rewrite Series_incr_1_aux. apply Series_ext => k. apply f_equal ; ring. intuition. move => k Hk ; intuition. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Lim_seq Rbar Hierarchy