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