Fix 2017 A1 (again)

The hypotheses were contradictory without the missing positivity guard
as the following succeeds without the change included here:
```
  exfalso
  have : IsQualifying S := hS.1
  rw [IsQualifying_def] at this
  obtain ⟨h₁, h₂, h₃, h₄⟩ := this
  have : -7 ∈ S := h₃ (-7) (h₄ 2 h₂)
  replace this : 0 < -7 := h₁ _ this
  linarith
```

This was previously "fixed" in c4512ca
but unfortunately an error remained.

lean4/src/putnam_2017_a1.lean

@@ -8,7 +8,7 @@ theorem putnam_2017_a1
     (IsQualifying_def : ∀ S, IsQualifying S ↔
       (∀ n ∈ S, 0 < n) ∧
       2 ∈ S ∧
-      (∀ n, n ^ 2 ∈ S → n ∈ S) ∧
+      (∀ n > 0, n ^ 2 ∈ S → n ∈ S) ∧
       (∀ n ∈ S, (n + 5) ^ 2 ∈ S))
     (S : Set ℤ)
     (hS : IsLeast IsQualifying S) :