proposition: Lemma Series_geom (q : R) : Rabs q < 1 -> Series (fun n => q ^ n) = / (1-q).
proof: Proof. move => Hq. apply is_series_unique. by apply is_series_geom. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Lim_seq Rbar Hierarchy