proposition: Theorem bernoulli_polynomial_val_0_1: forall n:nat,n<>1%nat -> bernoulli_polynomial n 0=bernoulli_polynomial n 1.
proof: Proof. intros n nneq1. unfold bernoulli_polynomial. transitivity ((bernoullicoeff n 0)+0). destruct n. unfold sum_f_R0. field. rewrite decomp_sum. unfold Init.Nat.pred. rewrite pow_O. rewrite Rmult_1_r. f_equal. rewrite<-(sumzero n) at 1. apply sum_eq. intros. simpl pow. field. apply Nat.lt_0_succ. destruct n. unfold sum_f_R0,bernoullicoeff. field. rewrite decomp_sum. unfold Init.Nat.pred. rewrite pow_O. rewrite Rmult_1_r. f_equal. destruct n. exfalso. apply nneq1. reflexivity. rewrite decomp_sum. rewrite pow1. rewrite Rmult_1_r. simpl Init.Nat.pred. unfold bernoullicoeff. fold bernoullicoeff. unfold bernoullicoeff at 1. fold bernoullicoeff. rewrite Rmult_comm. rewrite<-Rmult_assoc. rewrite scal_sum. rewrite Rmult_comm. rewrite scal_sum. rewrite<-sum_plus. rewrite<-(sumzero n) at 1. apply sum_eq. intros. rewrite pow1. simpl(INR 1). field. split; apply not_0_INR; discriminate. apply Nat.neq_0_lt_0. discriminate. apply Nat.neq_0_lt_0. discriminate. Qed.
imports: Reals