proposition: Lemma Rseq_pow_gt_1_cv : forall r, r > 1 -> Rseq_cv_pos_infty (Rseq_pow r).
proof: Proof. intros r Hr M. unfold Rseq_pow. destruct (Pow_x_infinity r) with (b := (M + 1)%R) as [N HN]. rewrite Rabs_right; lra. exists N; intros n Hn. rewrite <- Rabs_right. eapply Rlt_le_trans with (M + 1)%R; [lra|]. apply Rge_le; apply HN; assumption. left; apply pow_lt; lra. Qed.
imports: Lia Reals Rsequence_def Rsequence_base_facts Rsequence_cv_facts Rsequence_rel_facts Rsequence_rewrite_facts MyRIneq MyReals Lra