proposition: Lemma Series_incr_1 (a : nat -> R) : ex_series a -> Series a = a O + Series (fun k => a (S k)).
proof: Proof. move => Ha. apply is_series_unique. rewrite Rplus_comm. apply is_series_decr_1. rewrite /plus /opp /=. ring_simplify (Series (fun k : nat => a (S k)) + a 0%nat +- a 0%nat). apply Series_correct. by apply (ex_series_incr_1 a). Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Lim_seq Rbar Hierarchy