proposition: Lemma bisum_scal_mult : forall f a n, bisum (zr (Rmult a) f) n = a * (bisum f n).
proof: Proof. induction n. trivial. simpl bisum; rewrite IHn. unfold zr; ring. Qed.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia ZArith