proposition: Lemma ex_lim_seq_geom_p (q : R) : 1 < q -> ex_lim_seq (fun n => q ^ n).
proof: Proof. move => Hq ; exists p_infty ; by apply is_lim_seq_geom_p. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy