proposition: Lemma bisum_eq_compat_bounded : forall f g n, (forall z, ((-Z_of_nat n) <= z <= Z_of_nat n)%Z -> f z = g z) -> bisum f n = bisum g n.
proof: Proof. intros. induction n. simpl; apply H; simpl; lia. simpl. rewrite H; [ | simpl; split; [apply Zle_neg_pos | lia]]. rewrite H; [ | simpl; split; [lia | apply Zle_neg_pos]]. rewrite IHn. trivial. intros z [H1 H2]. apply H; split; eapply Z.le_trans; [ | apply H1 | apply H2 | ]; rewrite inj_S; lia. Qed.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia ZArith