rintro rfl
a✝ : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a✝.re a✝.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a✝
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hodd : Odd x
hfactor : x ∣ Zsqrtd.norm a
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
hneg1 : 1 ≤ Zsqrtd.norm a
⊢ x ≠ 0
a✝ : ℤ√(-3)
x : ℤ
hcoprime✝ : IsCoprime a✝.re a✝.im
hodd✝ : Odd x
hfactor✝ : x ∣ Zsqrtd.norm a✝
x✝ : ℕ
hx' : Int.natAbs x = x✝
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hneg1 : 1 ≤ Zsqrtd.norm a
hodd : Odd 0
hfactor : 0 ∣ Zsqrtd.norm a
IH :
  ∀ (m : ℕ),
    m < Int.natAbs 0 →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
⊢ False