calc
  4 < 3 * 2 := by norm_num
  _ ≤ 3 * p.im ^ 2 := (Int.mul_le_mul_of_nonneg_left hq' (by norm_num))
  _ ≤ p.re ^ 2 + 3 * p.im ^ 2 := (le_add_of_nonneg_left (pow_two_nonneg p.re))
  _ = p.norm := by
    rw [Zsqrtd.norm_def]
    ring
case a.h
p : ℤ√(-3)
hq : p.im ≠ 0
hq' : 1 + 1 ≤ p.im ^ 2
⊢ 4 < Zsqrtd.norm p
no goals