have h0' : 1 ≤ abs x := by rwa [← Int.sub_one_lt_iff, sub_self, abs_pos]
case h
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hodd : Odd x
hfactor : x ∣ a.norm
IH : ∀ m < x.natAbs, ∀ (a : ℤ√(-3)) (x : ℤ), IsCoprime a.re a.im → Odd x → x ∣ a.norm → x.natAbs = m → ∃ c, |x| = c.norm
hneg1 : 1 ≤ a.norm
h0 : x ≠ 0
⊢ ∃ c, |x| = c.norm
case h
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hodd : Odd x
hfactor : x ∣ a.norm
IH : ∀ m < x.natAbs, ∀ (a : ℤ√(-3)) (x : ℤ), IsCoprime a.re a.im → Odd x → x ∣ a.norm → x.natAbs = m → ∃ c, |x| = c.norm
hneg1 : 1 ≤ a.norm
h0 : x ≠ 0
h0' : 1 ≤ |x|
⊢ ∃ c, |x| = c.norm