proposition: Lemma bisum_not_in : forall f g j n, (j < (- Z_of_nat n) \/ Z_of_nat n < j)%Z -> bisum (fun i : Z => if Z.eq_dec i j then g j else f i) n = bisum f n.
proof: Proof. intros. apply bisum_eq_compat_bounded; intros. destruct H. destruct (Z.eq_dec z (- Z_of_nat (S n))). subst; destruct H0; rewrite inj_S in * |-; apply False_ind; lia. destruct (Z.eq_dec z j). subst; 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. destruct (Z.eq_dec z j). subst; apply False_ind; lia. trivial. Qed.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia ZArith