OEIS/211417: `formal_proof` anchor points at the form without `0 < D`

`OEIS/211417.lean`, `general_divisibility`:

```lean
theorem general_divisibility (r : ℕ) (hr : 1 ≤ r) :
∃ D : ℤ, 0 < D ∧ ∀ n : ℕ, (divisorProduct n r) ∣ (D * (a n : ℤ))
```

The `formal_proof` attribute anchors line 651 of the linked file. The declaration at that line is

```lean
theorem general_divisibility (r : ℕ) (hr : 1 ≤ r) :
∃ D : ℤ, ∀ n : ℕ, (divisorProduct n r) ∣ (D * (a n : ℤ))
```

without `0 < D`. The same file proves `general_divisibility_is_vacuous` with `D = 0`, and separately proves the statement that matches main as `general_divisibility_strong` (witness `Dwit r = (r!)^(r*r)` with `Dwit_pos`).

The docstring in main says the permalink "proves the non-vacuous form". The mathematics is there; the anchor is on the weak form.

Suggested fix: point the link at `general_divisibility_strong`. Happy to open the PR if that is the preferred route.

Found by fetching every `formal_proof` target and comparing the statement at the anchor with the statement in main (script to follow as a PR).

Inspect OEIS/211417.lean around general_divisibility, general_divisibility_strong, and the formal_proof anchor referenced by the main docstring. Update the link to general_divisibility_strong, then verify that the permalinked declaration includes 0 < D and matches the non-vacuous statement described in main.

Written by the indexing model from the issue text.