proposition: Theorem bernoulli_polynomial_derivable_pt_lim: forall n:nat,forall x:R, derivable_pt_lim (bernoulli_polynomial (S n)) x ((bernoulli_polynomial n x)*(INR (S n))).
proof: Proof. intros. erewrite (_:(_*(INR (S n))=_)). apply derivable_pt_lim_fs. apply Nat.lt_0_succ. Unshelve. unfold Init.Nat.pred. rewrite Rmult_comm at 1. unfold bernoullicoeff. fold bernoullicoeff. unfold bernoulli_polynomial. rewrite scal_sum. apply sum_eq. intros. repeat rewrite<-Rmult_assoc. field. apply not_0_INR. discriminate. Qed.
imports: Reals