apply even_iff_two_dvd.mp X
f : ℤ
hodd : Odd f
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = a.norm
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, |f'| = p.norm
IH :
  ∀ m < g.natAbs,
    ∀ (a : ℤ√(-3)) (g : ℤ),
      ¬g = 0 → f * g = a.norm → (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, |f'| = p.norm) → g.natAbs = m → ∃ p, |f| = p.norm
H : ¬Even a.norm
h : ¬g.natAbs = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
this : p ∣ a.norm
X : Even p
⊢ 2 ∣ p
no goals