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 a.norm.natAbs)
case h
n : ℕ
ih : ∀ m < n, ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → a.norm.natAbs = m → Even (evenFactorExp m)
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : a.norm.natAbs = n
⊢ Even (evenFactorExp n)