proposition: Lemma bound1_cv : Rseq_cv bound1 0.
proof: Proof. replace 0 with (0 + 0) by ring. eapply Rseq_cv_eq_compat. 2:apply Rseq_cv_plus_compat; [apply bound1'_cv | apply bound1c_cv]. intro; unfold Rseq_plus, bound1', bound1c, bound1. 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