have hg'pos : g' ≠ 0 := right_ne_zero_of_mul hgpos
case pos.intro.intro
f : ℤ
hodd : Odd f
a : ℤ√(-3)
H : Even a.norm
c : ℤ√(-3)
hc : a.norm = 4 * c.norm
g' : ℤ
hgpos : 4 * g' ≠ 0
hfactor : f * (4 * g') = a.norm
hnotform : ∀ (f' : ℤ), f' ∣ 4 * g' → Odd f' → ∃ p, |f'| = p.norm
IH :
  ∀ m < (4 * 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
⊢ ∃ p, |f| = p.norm
case pos.intro.intro
f : ℤ
hodd : Odd f
a : ℤ√(-3)
H : Even a.norm
c : ℤ√(-3)
hc : a.norm = 4 * c.norm
g' : ℤ
hgpos : 4 * g' ≠ 0
hfactor : f * (4 * g') = a.norm
hnotform : ∀ (f' : ℤ), f' ∣ 4 * g' → Odd f' → ∃ p, |f'| = p.norm
IH :
  ∀ m < (4 * 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
hg'pos : g' ≠ 0
⊢ ∃ p, |f| = p.norm