proposition: Lemma bisum_eq_compat : forall f g n, (forall z, f z = g z) -> bisum f n = bisum g n.
proof: Proof. intros. induction n. simpl; apply H. simpl; do 2 rewrite H. rewrite IHn; trivial. Qed.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia ZArith