. linarith
case this
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
⊢ u ≠ 1

k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
⊢ ∃ x, x < PrimeRange.prod (Nat.succ (Nat.succ k)) + u ∧ 2 ≤ x ∧ x ∣ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
⊢ ∃ x, x < PrimeRange.prod (Nat.succ (Nat.succ k)) + u ∧ 2 ≤ x ∧ x ∣ PrimeRange.prod (Nat.succ (Nat.succ k)) + u