proposition: Lemma bisum_minus : forall f g n, bisum (zr2 Rminus f g) n = bisum f n - bisum g n.
proof: Proof. induction n. trivial. simpl bisum; rewrite IHn. unfold zr2; ring. Qed.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia ZArith