rw [Zsqrtd.norm_def, H, MulZeroClass.mul_zero, sub_zero, ← pow_two] at h
p : ℤ√(-3)
h : OddPrimeOrFour p.norm.natAbs
hcoprime : IsCoprime p.re p.im
H : p.im = 0
⊢ False
p : ℤ√(-3)
h : OddPrimeOrFour (p.re ^ 2).natAbs
hcoprime : IsCoprime p.re p.im
H : p.im = 0
⊢ False