proposition: Lemma Rseq_cv_bounded : forall Un l, l <> 0 -> Rseq_cv Un l -> forall k, 1 < k -> Rseq_eventually (fun un => forall n, (Rabs l) / k < Rabs (un n)) Un.
proof: Proof. intros Un l l_neq Hl k k_lb. pose (eps := (k - 1) / k * Rabs l). assert (eps_pos : 0 < eps). unfold eps ; apply Rmult_lt_0_compat ; [unfold Rdiv ; apply Rlt_mult_inv_pos ; [ | apply Rlt_trans with 1] | apply Rabs_pos_lt] ; intuition (auto with real) ; lra. destruct (Hl _ eps_pos) as [N HN] ; exists N ; intros n. apply Rle_lt_trans with (Rabs l - eps). unfold eps, Rdiv ; right ; field ; apply Rgt_not_eq ; apply Rlt_trans with 1 ; lra. apply R_dist_gt_r ; apply HN ; intuition (auto with arith). Qed.
imports: Reals Rsequence_def Rpser_def Rpser_def_simpl Rpser_base_facts Rsequence_facts Rsequence_sums_facts Rsequence_rewrite_facts Rpow_facts Lra PeanoNat MyRIneq MyNeq Rinterval RFsequence RFsequence_facts Tactics