proposition: Lemma bisumsum_one_step : forall f n m, bisum (fun i => bisum (f i) (S n)) m = bisum (fun i => bisum (f i) n) m + bisum (fun i => f i (Z_of_nat (S n)) ) m + bisum (fun i => f i (- Z_of_nat (S n))%Z ) m.
proof: Proof. intros. simpl. repeat rewrite <- bisum_plus. apply bisum_eq_compat; intros. trivial. Qed.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia ZArith