exact not_prime_pow one_lt_two.ne' hprime
case inr.intro.intro
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hfactor : x ∣ a.norm
hodd : Odd x
c : ℤ√(-3)
hprime : Prime (c.re ^ 2)
hc : c.re ^ 2 = ↑x.natAbs
H : c.im = 0
⊢ False
no goals