proposition: Lemma bisumsum_eq_compat : forall f g n, (forall x y, f x y = g x y) -> bisumsum f n = bisumsum g n.
proof: Proof. intros; apply bisum_eq_compat. intros; apply bisum_eq_compat. apply H. Qed.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia ZArith