right
case h
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even a.norm
ha : Odd a.re
hb : Odd a.im
v : ℤ
hv : a.re = 4 * v - a.im
⊢ a = { re := 1, im := 1 } * { re := v - a.im, im := v } ∨ a = { re := 1, im := -1 } * { re := v - a.im, im := v }
case h.h
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even a.norm
ha : Odd a.re
hb : Odd a.im
v : ℤ
hv : a.re = 4 * v - a.im
⊢ a = { re := 1, im := -1 } * { re := v - a.im, im := v }