fact: Fixpoint bisum (f : Z -> R) (N : nat) := match N with | O => f Z0 | S n => (bisum f n) + f (Z_of_nat N) + f (- Z_of_nat N)%Z end.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia ZArith