proposition: Lemma Sum_bntg_neg : Rser_cv bntg_neg (sumbntg + 1).
proof: Proof. apply Rser_cv_shift_rev2. eapply Rser_cv_ext. apply bntg_shift_neg_compat. replace (sumbntg + 1 - bntg_neg 0) with sumbntg by (compute; field). apply Sum_bntg. Qed.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia ZArith