proposition: Lemma Rseq_pow_lt_1_cv : forall r, 0 <= r < 1 -> Rseq_cv (Rseq_pow r) 0.
proof: Proof. intros r [Hl Hr] eps Heps. unfold R_dist; unfold Rseq_pow. assert (exists N, forall n, (n >= N)%nat -> Rabs (r ^ n) < eps). apply pow_lt_1_zero; [rewrite Rabs_right|]; try apply Rle_ge; assumption. destruct H as [N H]. exists N; intros n Hn. rewrite Rminus_0_r. apply H; assumption. Qed.
imports: Lia Reals Rsequence_def Rsequence_base_facts Rsequence_cv_facts Rsequence_rel_facts Rsequence_rewrite_facts MyRIneq MyReals Lra