obtain h4 | ⟨p, hpprime, hpdvd, hpodd⟩ := Nat.four_dvd_or_exists_odd_prime_and_dvd_of_two_lt n2
n : ℕ
n2 : 2 < n
⊢ ∃ p, p ∣ n ∧ OddPrimeOrFour p
case inl
n : ℕ
n2 : 2 < n
h4 : 4 ∣ n
⊢ ∃ p, p ∣ n ∧ OddPrimeOrFour p

case inr.intro.intro.intro
n : ℕ
n2 : 2 < n
p : ℕ
hpprime : p.Prime
hpdvd : p ∣ n
hpodd : Odd p
⊢ ∃ p, p ∣ n ∧ OddPrimeOrFour p