proposition: Lemma kthpowers : forall n:nat, forall x:R, x^n*(INR (S n))=(bernoulli_polynomial (S n) (x+1))-(bernoulli_polynomial (S n) x).
proof: Proof. induction n. intro. unfold bernoulli_polynomial,sum_f_R0,bernoullicoeff. unfold sum_f_R0,INR,pow. field. apply (primitive_eq _ _ (fun x=>(INR (S n))*x^n*(INR (S (S n)))) ). intro x. apply (derivable_pt_lim_scal_right (fun x=>x^(S n)) x _ (INR (S (S n)))). pose proof (derivable_pt_lim_pow x (S n)) as derpow. unfold Init.Nat.pred in derpow. apply derpow. intro x. erewrite(_:(INR (S n) * x ^ n * INR (S (S n)))=_). apply derivable_pt_lim_minus. apply bernoulli_polynomial_derivable_pt_lim_shift. apply bernoulli_polynomial_derivable_pt_lim. unfold pow. repeat rewrite Rmult_0_l. rewrite bernoulli_polynomial_val_0_1. rewrite Rplus_0_l. rewrite Rminus_diag_eq; reflexivity. discriminate. Unshelve. rewrite(Rmult_comm (INR (S n))). rewrite IHn. field. Qed.
imports: Reals