exact not_isCoprime_zero_zero hcoprime
x : ℤ
hodd : Odd x
IH : ∀ m < x.natAbs, ∀ (a : ℤ√(-3)) (x : ℤ), IsCoprime a.re a.im → Odd x → x ∣ a.norm → x.natAbs = m → ∃ c, |x| = c.norm
hcoprime : IsCoprime 0 0
hfactor : x ∣ Zsqrtd.norm 0
⊢ False
no goals