proposition: Lemma is_lim_seq_geom (q : R) : Rabs q < 1 -> is_lim_seq (fun n => q ^ n) 0.
proof: Proof. intros Hq. apply is_lim_seq_spec. move => [e He] /=. case: (pow_lt_1_zero q Hq e He) => N H. exists N => n Hn. rewrite Rminus_0_r ; by apply H. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy