proposition: Lemma sum_div : forall (x : R), x <> 0 -> forall (An : nat -> R) (N : nat), sum_f_R0 (fun n => An n / x) N = (sum_f_R0 An N) / x.
proof: Proof. intros x H An N. induction N. reflexivity. simpl. rewrite IHN. field. assumption. Qed.
imports: ZArith Reals Lia Lra DiscrR Rfunctions