case h
n p : ℕ
⊢ eval (↑n) (bernoulli (succ p)) - _root_.bernoulli (succ p) = (↑p + 1) * ∑ k in range n, ↑k ^ p
n p : ℕ
⊢ eval (↑n) (bernoulli (succ p)) = _root_.bernoulli (succ p) + (↑p + 1) * ∑ k in range n, ↑k ^ p
apply eq_add_of_sub_eq'
no goals
case h
n p : ℕ
⊢ eval (↑n) (bernoulli (succ p)) - _root_.bernoulli (succ p) = (↑p + 1) * ∑ k in range n, ↑k ^ p
rw [sum_range_pow_eq_bernoulli_sub]