proposition: Lemma bisum_strip_nothing : forall f n j, ((- Z_of_nat (S n)) = j \/ j = Z_of_nat (S n))%Z -> bisum_strip' f j n = bisum f n.
proof: Proof. intros. unfold bisum_strip'. apply bisum_eq_compat_bounded; intros. destruct H; subst. destruct (Z.eq_dec z (- Z_of_nat (S n))). subst; destruct H0; rewrite inj_S in * |- ; apply False_ind; lia. trivial. destruct (Z.eq_dec z (Z_of_nat (S n))). subst; destruct H0; rewrite inj_S in * |- ; apply False_ind; lia. trivial. Qed.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia ZArith