simp
k u : ℕ
a✝ : 2 ≤ u ∧ u ≤ Nat.succ k
⊢ ¬(2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u ∧
      ∀ (m : ℕ),
        2 ≤ m → m < PrimeRange.prod (Nat.succ (Nat.succ k)) + u → ¬m ∣ PrimeRange.prod (Nat.succ (Nat.succ k)) + u)
k u : ℕ
a✝ : 2 ≤ u ∧ u ≤ Nat.succ k
⊢ 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u →
    ∃ x, x < PrimeRange.prod (Nat.succ (Nat.succ k)) + u ∧ 2 ≤ x ∧ x ∣ PrimeRange.prod (Nat.succ (Nat.succ k)) + u