proposition: Lemma sum_bisum : forall n f, bisum f (S n) = sum_f_R0 (fun i => f (Z_of_nat i)) (S n) + sum_f_R0 (fun i => f (- Z_of_nat (S i))%Z) n.
proof: Proof. intros. induction n. trivial. replace (bisum f (S (S n))) with (bisum f (S n) + f (Zpos (Pos.succ (P_of_succ_nat n))) + f (Zneg (Pos.succ (P_of_succ_nat n)))) by trivial. rewrite IHn. simpl. ring. Qed.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia ZArith