rw [Nat.prime_iff_prime_int] at hp
case intro.inr.intro.intro.intro
n : ℕ
n2 : 2 < n
p : ℕ
hp : Nat.Prime p
hdvd : p ∣ n
hodd : Odd p
⊢ ∃ p, p ∣ ↑n ∧ OddPrimeOrFour p
case intro.inr.intro.intro.intro
n : ℕ
n2 : 2 < n
p : ℕ
hp : Prime ↑p
hdvd : p ∣ n
hodd : Odd p
⊢ ∃ p, p ∣ ↑n ∧ OddPrimeOrFour p