proposition: Lemma is_lim_seq_geom_p (q : R) : 1 < q -> is_lim_seq (fun n => q ^ n) p_infty.
proof: Proof. intros Hq. apply is_lim_seq_spec. move => M /=. case: (fun Hq => Pow_x_infinity q Hq (M+1)) => [ | N H]. by apply Rlt_le_trans with (1 := Hq), Rle_abs. exists N => n Hn. apply Rlt_le_trans with (M+1). rewrite -{1}(Rplus_0_r M) ; by apply Rplus_lt_compat_l, Rlt_0_1. rewrite -(Rabs_pos_eq (q^n)). by apply Rge_le, H. by apply pow_le, Rlt_le, Rlt_trans with (1 := Rlt_0_1). Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy