proposition: Lemma is_series_incr_n (a : nat -> V) (n : nat) (l : V) : (0 < n)%nat -> is_series a (plus l (sum_n a (pred n))) -> is_series (fun k => a (n + k)%nat) l.
proof: Proof. case: n => /= [ | n] Hn Ha. by apply Nat.lt_irrefl in Hn. clear Hn. elim: n l Ha => [ | n IH] l Ha. rewrite sum_O in Ha. by apply is_series_incr_1. apply is_series_ext with (fun k : nat => a (S (n + S k))). move => k ; apply f_equal ; ring. apply (is_series_incr_1 (fun k : nat => a (S (n + k))) l). rewrite Nat.add_0_r. apply IH. replace (plus (plus l (a (S n))) (sum_n a n)) with (plus l (sum_n a (S n))). assumption. rewrite <- plus_assoc, sum_Sn; apply f_equal; simpl; apply plus_comm. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Lim_seq Rbar Hierarchy