rw [Nat.prime_def_lt] at np
case neg.h
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m
h : 2 ≤ n
np : ¬n.Prime
⊢ ∃ p, p.Prime ∧ p ∣ n
case neg.h
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m
h : 2 ≤ n
np : ¬(2 ≤ n ∧ ∀ m < n, m ∣ n → m = 1)
⊢ ∃ p, p.Prime ∧ p ∣ n