proposition: Lemma Lim_seq_geom_p (q : R) : 1 < q -> Lim_seq (fun n => q ^ n) = p_infty.
proof: Proof. intros. apply is_lim_seq_unique. by apply is_lim_seq_geom_p. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy