proposition: Theorem bernoulli_polynomial_derivable_pt_lim_shift: forall n:nat,forall x:R, derivable_pt_lim (fun x=> (bernoulli_polynomial (S n) (x+1))) x ((bernoulli_polynomial n (x+1))*(INR (S n))).
proof: Proof. unfold derivable_pt_lim. intros. destruct (bernoulli_polynomial_derivable_pt_lim n (x+1) eps) as [delta der]. assumption. exists delta. intros. enough(x+h+1=x+1+h) as ->. apply der; assumption. field. Qed.
imports: Reals