proposition: Lemma sum_kthpowers : forall r:nat, forall n:nat, (0<r)%nat-> sum_f_R0 (fun k => ((INR k)^r)%R) n =((bernoulli_polynomial (S r) (INR n+1))-(bernoulli_polynomial (S r) 0))/(INR r+1).
proof: Proof. intros r n rneq0. induction n. unfold INR. fold INR. rewrite bernoulli_polynomial_val_0_1. rewrite Rplus_0_l. unfold sum_f_R0. unfold pow,INR. fold INR. fold pow. induction r. exfalso. apply (Nat.neq_0_lt_0 0). assumption. reflexivity. unfold pow. fold pow. field. rewrite<-S_INR. apply not_0_INR. discriminate. apply not_eq_S. intro. apply Nat.neq_0_lt_0 in rneq0. contradiction. unfold sum_f_R0. fold sum_f_R0. rewrite IHn. enough(INR (S n) ^ r=(INR (S n) ^r * (INR (S r)))/(INR (S r))) as ->. rewrite kthpowers. repeat rewrite<-S_INR. field. apply not_0_INR. discriminate. field. apply not_0_INR. discriminate. Qed.
imports: Reals