use -a
case inl
d : ℤ
a : ℤ√d
him : a.im ≠ 0
hre : a.re ≤ 0
⊢ ∃ c, a.norm = c.norm ∧ 0 ≤ c.re ∧ c.im ≠ 0
case h
d : ℤ
a : ℤ√d
him : a.im ≠ 0
hre : a.re ≤ 0
⊢ a.norm = (-a).norm ∧ 0 ≤ (-a).re ∧ (-a).im ≠ 0