proposition: Lemma scal_sum1 : forall (An : nat -> R) (N : nat) (x : R), x * (sum_f_R0 An N) = sum_f_R0 (fun i => x * (An i)) N.
proof: Proof. intros An N x. induction N. reflexivity. simpl. ring_simplify. rewrite IHN. ring. Qed.
imports: ZArith Reals Lia Lra DiscrR Rfunctions