rw [Zsqrtd.norm_def, him, MulZeroClass.mul_zero, sub_zero, ← sq, ← sq_abs, hcoprime] at hfour
p : ℤ√(-3)
hcoprime : abs p.re = 1
hfour : Zsqrtd.norm p = 4
him : p.im = 0
⊢ False
p : ℤ√(-3)
hcoprime : abs p.re = 1
hfour : 1 ^ 2 = 4
him : p.im = 0
⊢ False