rw [Zsqrtd.norm_def, neg_mul, neg_mul, sub_neg_eq_add]
case H.inr.h
a : ℤ√(-3)
h : abs a.re ≠ 1
H : abs a.re > 1
⊢ 1 < Zsqrtd.norm a
case H.inr.h
a : ℤ√(-3)
h : abs a.re ≠ 1
H : abs a.re > 1
⊢ 1 < a.re * a.re + 3 * a.im * a.im