HOL-ex.HarmonicSeries