by_cases H : 2 * c.natAbs < x.natAbs
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
⊢ ∃ m c, c + m * x = a ∧ 2 * natAbs c < natAbs x
case pos
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : 2 * natAbs c < natAbs x
⊢ ∃ m c, c + m * x = a ∧ 2 * natAbs c < natAbs x

case neg
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : ¬2 * natAbs c < natAbs x
⊢ ∃ m c, c + m * x = a ∧ 2 * natAbs c < natAbs x