fix: align Dusart lemma_5_10a with 1-indexed prime numbering

[Chessing234]

Fixes #1129

Bug

lemma_5_10a used nth_prime' k with paper index k ≥ 4, but nth_prime' is 0-indexed. At k = 4 this claims 11 ≤ 4 log 11, which is false.

Root cause

Dusart's p_k is 1-indexed; the Lean formalization used the paper index directly as the nth_prime' argument.

Why this fix is correct

The k-th prime in the paper is nth_prime' (k - 1). For k = 4 this gives p_4 = 7 and 7 ≤ 4 log 7, matching Lemma 5.10.

Test plan

• lake build PrimeNumberTheoremAnd.IEANTN.Dusart

Made with Cursor