proposition: Lemma Series_incr_1_aux (a : nat -> R) : a O = 0 -> Series a = Series (fun k => a (S k)).
proof: Proof. move => Ha. rewrite /Series. rewrite -Lim_seq_incr_1. apply f_equal, Lim_seq_ext => n. rewrite /sum_n sum_n_m_S sum_Sn_m. rewrite Ha ; by apply Rplus_0_l. by apply Nat.le_0_l. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Lim_seq Rbar Hierarchy