feat(number_theory/bernoulli): faulhaber' (#6684)
This deduces an alternative form `faulhaber'` of Faulhaber's theorem from `faulhaber`. In this version, we
1. sum over `1` to `n` instead of `0` to `n - 1` and
2. use `bernoulli'` instead of `bernoulli`.
Arguably, this is the more common form one finds Faulhaber's theorem in the literature.
Co-authored-by: Moritz Firsching <firsching@google.com>
Co-authored-by: Benjamin Davidson <68528197+benjamindavidson@users.noreply.github.com>
