Reciprocals of a block of consecutive integers never sum to an integer

For every $n \ge 1$ and every $k \ge 2$,

This is Kürschák's theorem, stated in the equivalent form $H_{n+k-1} - H_{n-1} \notin \mathbb{Z}$. Mathlib already contains the special case $n = 1$ (harmonic_not_int, that $H_m \notin \mathbb{Z}$ for $m \ge 2$); the statement here is the general block version. Erdős' 1932 paper generalises it further, from blocks of consecutive integers to arithmetic progressions.

The result is the substance behind the gap-two bound for Erdős Problem 287: a representation of $1$ all of whose consecutive differences equal one has denominators forming exactly such a block.

Formalization note. ¬ ∃ m : ℤ, S = (m : ℚ) is used rather than a predicate such as Rat.isInt, so that the assertion is transparent. Both hypotheses are needed: the sum of a single reciprocal $1/1$ is an integer, and $n = 0$ would make the first summand undefined as a reciprocal (1/0 = 0 in Lean).