exact zero_lt_one.trans h
x : ℤ
hodd : Odd x
h : 1 < abs x
c m : ℤ√(-3)
h2 : Zsqrtd.norm c < x ^ 2
hcoprime : IsCoprime (c + m * ↑x).re (c + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c + m * ↑x)
y : ℤ
hy : Zsqrtd.norm c = x * y
⊢ 0 < abs x
no goals