obtain ⟨u, huvcoprime, huvprod⟩ := step1' hcoprime (Int.natAbs_even.mp hparity)
case pos
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
hparity : Even a.norm.natAbs
⊢ Even (evenFactorExp n)
case pos.intro.intro
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
hparity : Even a.norm.natAbs
u : ℤ√(-3)
huvcoprime : IsCoprime u.re u.im
huvprod : a.norm = 4 * u.norm
⊢ Even (evenFactorExp n)