refine' ⟨⟨1, 1⟩, _, zero_le_one, one_ne_zero⟩
case inl
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hfactor : x ∣ a.norm
hx : x.natAbs = 4
⊢ ∃ c, |x| = c.norm ∧ 0 ≤ c.re ∧ c.im ≠ 0
case inl
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hfactor : x ∣ a.norm
hx : x.natAbs = 4
⊢ |x| = { re := 1, im := 1 }.norm