proposition: Lemma bound_eq : forall N, abound (S N) = bound1 (S N) + bound2 (S N).
proof: Proof. intros. unfold abound, bound1, bound2. simpl (pred (S N)). do 2 rewrite scal_sum. erewrite sum_eq. apply sum_plus. intros n H. replace (S N - S n + 1)%nat with (S N - n)%nat by lia. rewrite abound_eq; try lia. replace (S N - S n + 1)%nat with (S N - n)%nat by lia. field; INR_solve. Qed.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia ZArith