proposition: Lemma abound_cv : Rseq_cv abound 0.
proof: Proof. replace 0 with (0 + 0) by ring. eapply Rseq_cv_asymptotic_eq_compat. 2:apply Rseq_cv_plus_compat; [apply bound1_cv | apply bound2_cv]. exists (S O). intros n Hb. assert (H : exists n', n = S n'). exists (pred n); symmetry; apply Nat.lt_succ_pred with O; apply Hb. destruct H; subst. unfold Rseq_plus. symmetry; apply bound_eq. Qed.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia ZArith