suffices H : abs a.re = 1 by
  refine' ⟨H, _⟩
  rw [Zsqrtd.norm_def, mul_assoc, ← Int.natAbs_mul_self' a.re, ← Int.abs_eq_natAbs, H, one_mul,
    neg_mul, sub_neg_eq_add, add_right_eq_self, mul_eq_zero, mul_self_eq_zero] at h
  exact h.resolve_left three_ne_zero
a : ℤ√(-3)
h : a.norm = 1
⊢ |a.re| = 1 ∧ a.im = 0
a : ℤ√(-3)
h : a.norm = 1
⊢ |a.re| = 1