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