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