proposition: Lemma bound2_cv : Rseq_cv bound2 0.
proof: Proof. replace 0 with (0 + 0) by ring. eapply Rseq_cv_eq_compat. 2:apply Rseq_cv_plus_compat; [apply bound2'_cv | apply bound2c_cv]. intro; unfold Rseq_plus, bound2', bound2c, bound2. rewrite <- Rmult_plus_distr_l. inject. rewrite <- sum_plus. apply Rseq_sum_ext; intro; trivial. Qed.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia ZArith