induction' hn : a.norm.natAbs using Nat.strong_induction_on with n ih generalizing a
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
⊢ Even (evenFactorExp (Zsqrtd.norm a))
case h
a✝ : ℤ√(-3)
hcoprime✝ : IsCoprime a✝.re a✝.im
x✝ : ℕ
hn✝ : Int.natAbs (Zsqrtd.norm a✝) = x✝
n : ℕ
ih :
  ∀ (m : ℕ),
    m < n → ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → Int.natAbs (Zsqrtd.norm a) = m → Even (evenFactorExp (Zsqrtd.norm a))
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : Int.natAbs (Zsqrtd.norm a) = n
⊢ Even (evenFactorExp (Zsqrtd.norm a))