proposition: Lemma Rseq_cv_neg_infty_criteria : forall An d, d < 0 -> (forall n, An n <= 0) -> (forall M, exists N, (N >= M)%nat /\ Rseq_sum (Rseq_shifts An M) (N - M) <= d) -> Rseq_cv_neg_infty (Rseq_sum An).
proof: Proof. intros An d d_neg An_neg HAn ; apply Rseq_cv_neg_infty_eq_compat with (- Rseq_sum (- An)). intro n ; unfold Rseq_opp at 1 ; rewrite Rseq_sum_opp_compat ; unfold Rseq_opp ; apply Ropp_involutive. apply Rseq_cv_pos_infty_opp_compat, Rseq_cv_pos_infty_criteria with (- d)%R. lra. intro n ; unfold Rseq_opp ; pose (An_neg n) ; lra. intro M ; destruct (HAn M) as [N [N_lb HN]] ; exists N ; split. assumption. rewrite Rseq_sum_ext with (Vn := - Rseq_shifts An M). rewrite Rseq_sum_opp_compat ; apply Ropp_le_contravar, HN. apply Rseq_shifts_opp_compat. Qed.
imports: Lia Rsequence_def Rsequence_base_facts Rsequence_cv_facts Rsequence_rewrite_facts Rpser_def Rpser_def_simpl MyRIneq MyNat Lra