proposition: Lemma is_series_geom (q : R) : Rabs q < 1 -> is_series (fun n => q ^ n) (/ (1-q)).
proof: Proof. move => Hq. apply filterlim_ext with (fun n => (1-q^(S n)) / (1-q)). move => n. rewrite sum_n_Reals; rewrite tech3. reflexivity. apply Rlt_not_eq. apply Rle_lt_trans with (2 := Hq). apply Rle_abs. change (is_lim_seq (fun n : nat => (1 - q ^ S n) / (1 - q)) (/(1-q))). replace ((/ (1 - q))) with (real (Rbar_mult (Rbar_minus 1 0) (/ (1 - q)))). unfold Rdiv. apply (is_lim_seq_scal_r (fun n : nat => (1 - q ^ S n)) (/ (1 - q)) (Rbar_minus 1 0)). apply is_lim_seq_minus'. by apply is_lim_seq_const. apply (is_lim_seq_incr_1 (fun n => q^n)). by apply is_lim_seq_geom. simpl; ring. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Lim_seq Rbar Hierarchy