refine' ⟨(a + abs x) / x, c - abs x, _, _⟩
case neg
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : natAbs x ≤ 2 * natAbs (a % x)
⊢ ∃ m c, c + m * x = a ∧ 2 * natAbs c < natAbs x
case neg.refine'_1
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : natAbs x ≤ 2 * natAbs (a % x)
⊢ c - abs x + (a + abs x) / x * x = a

case neg.refine'_2
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : natAbs x ≤ 2 * natAbs (a % x)
⊢ 2 * natAbs (c - abs x) < natAbs x