proposition: Lemma Sum_bnz : Rseq_cv Bn (2 * sumbntg).
proof: Proof. eapply Rseq_cv_eq_compat; [symmetry; apply bisum_bnz_bntg | ]. replace (2 * sumbntg) with (sumbntg + ((sumbntg + 1) - 1)) by field. apply Rseq_cv_plus_compat; [apply Sum_bntg | ]. apply Rseq_cv_minus_compat; [ | apply Rseq_constant_cv]. apply Sum_bntg_neg. Qed.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia ZArith