exfalso
case neg.inr
x A : ℤ√(-3)
hx : 0 ≤ x.re
hA : 0 ≤ A.re
u : (ℤ√(-3))ˣ
v : ℤ
hu : x * ↑v = star A
hv1 : ↑u = ↑v
hxre : ¬x.re = 0
habsv : v = -1
⊢ x = A ∨ x = star A
case neg.inr
x A : ℤ√(-3)
hx : 0 ≤ x.re
hA : 0 ≤ A.re
u : (ℤ√(-3))ˣ
v : ℤ
hu : x * ↑v = star A
hv1 : ↑u = ↑v
hxre : ¬x.re = 0
habsv : v = -1
⊢ False