proposition: Lemma Rseq_pow_lt_1_cv_strong : forall r, Rabs r < 1 -> Rseq_cv (Rseq_pow r) 0.
proof: Proof. intros r H eps eps_pos ; assert (Hx : 0 <= Rabs r < 1) by (split ; [apply Rabs_pos | assumption]) ; destruct (Rseq_pow_lt_1_cv _ Hx _ eps_pos) as [N HN] ; exists N ; intros n n_lb. eapply Rle_lt_trans ; [| eapply HN ; eassumption]. right ; unfold R_dist, Rseq_pow ; do 2 rewrite Rminus_0_r, <- RPow_abs ; rewrite Rabs_Rabsolu ; reflexivity. Qed.
imports: Lia Reals Rsequence_def Rsequence_base_facts Rsequence_cv_facts Rsequence_rel_facts Rsequence_rewrite_facts MyRIneq MyReals Lra