proposition: Lemma bisum_reverse : forall f n, bisum f n = bisum (fun i => f (- i)%Z) n.
proof: Proof. induction n. trivial. simpl. rewrite IHn. ring. Qed.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia ZArith