simp only [Zsqrtd.norm_def, mul_one, abs_of_pos, zero_lt_four, sub_neg_eq_add]
case inl
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hfactor : 4 ∣ Zsqrtd.norm a
⊢ Abs.abs 4 = Zsqrtd.norm { re := 1, im := 1 }
no goals