fix(ErdosProblems/961): assume k positive

FormalConjectures/ErdosProblems/961.lean

@@ -33,19 +33,32 @@ Sylvester and Schur [Er34] proved that every set of $k$ consecutive integers gre
 contains an integer divisible by a prime greater than $k$, i.e. not $(k+1)$-smooth.
 -/
 @[category research solved, AMS 11]
-theorem erdos_961.sylvester_schur (k : ℕ) : Erdos961Prop k k := by
+theorem erdos_961.sylvester_schur (k : ℕ) (hk : 0 < k) : Erdos961Prop k k := by
   sorry
 
+@[category test, AMS 11]
+theorem erdos_961.sylvester_schur_1_1 : Erdos961Prop 1 1 := by
+  intro m hm
+  use m
+  constructor
+  · simp
+  · rw [Nat.mem_smoothNumbers]
+    push_neg
+    intro hm0
+    obtain ⟨p, hp, hpm⟩ := Nat.exists_prime_and_dvd (by omega : m ≠ 1)
+    exact ⟨p, (Nat.mem_primeFactorsList hm0).mpr ⟨hp, hpm⟩, hp.two_le⟩
+
 @[category research solved, AMS 11]
-theorem erdos_961.well_defined (k : ℕ) : ∃ n, Erdos961Prop k n := by
+theorem erdos_961.well_defined (k : ℕ) (hk : 0 < k): ∃ n, Erdos961Prop k n := by
   use k
-  exact erdos_961.sylvester_schur k
+  exact erdos_961.sylvester_schur k hk
 
 /--
 For $k$, let $f(k)$ be the minimal $n$ such that every set of $n$ consecutive integers $>k$ contains
 an integer divisible by a prime $>k$, i.e. not $(k+1)$-smooth.
 -/
-noncomputable def f (k : ℕ) : ℕ := Nat.find (erdos_961.well_defined k)
+noncomputable def f (k : ℕ) : ℕ :=
+  if hk : 0 < k then Nat.find (erdos_961.well_defined k hk) else 0
 
 /--
 It is conjectured that $f(k) \ll (\log k)^O(1)$.