proposition: Lemma bisum_strip_equiv : forall f n j, ((- Z_of_nat n) <= j <= Z_of_nat n)%Z -> bisum_strip f j n = bisum_strip' f j n.
proof: Proof. intros. unfold bisum_strip, bisum_strip'. replace (bisum (fun i : Z => if Z.eq_dec i j then 0 else f i) n) with (bisum (fun i : Z => if Z.eq_dec i j then Zzero j else f i) n). rewrite bisum_in. unfold Zzero; ring. apply H. unfold Zzero; trivial. Qed.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia ZArith