simp only [Zsqrtd.norm_def, mul_one, sub_neg_eq_add, Int.abs_eq_natAbs, hx]
case inl
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hfactor : x ∣ a.norm
hx : x.natAbs = 4
⊢ |x| = { re := 1, im := 1 }.norm
case inl
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hfactor : x ∣ a.norm
hx : x.natAbs = 4
⊢ ↑4 = 1 + 3