harmonic_pos

theorem harmonic_pos : ∀ {n : ℕ}, n ≠ 0 → 0 < harmonic n

The theorem `harmonic_pos` asserts that for every natural number `n` which is not zero, the nth harmonic number is positive. The nth harmonic number is defined as the sum of reciprocals of all natural numbers from 1 to `n`.

More concisely: For every natural number `n` greater than zero, the sum of the reciprocal of each number from 1 to `n` is positive.