induction' hg : g.natAbs using Nat.strong_induction_on with g'' IH generalizing a g
a : ℤ√(-3)
f g : ℤ
hodd : Odd f
hgpos : g ≠ 0
hfactor : f * g = a.norm
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, |f'| = p.norm
⊢ ∃ p, |f| = p.norm
case h
f : ℤ
hodd : Odd f
g'' : ℕ
IH :
  ∀ m < g'',
    ∀ (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
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = a.norm
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, |f'| = p.norm
hg : g.natAbs = g''
⊢ ∃ p, |f| = p.norm