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