have h0' : x ≠ 0 := by
  rintro rfl
  simp only [even_zero, not_true, Int.odd_iff_not_even] at hodd
a x : ℤ
hodd : Odd x
⊢ ∃ m c, c + m * x = a ∧ 2 * natAbs c < natAbs x
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
⊢ ∃ m c, c + m * x = a ∧ 2 * natAbs c < natAbs x