rw [Int.add_ediv_of_dvd_right this, add_mul, Int.ediv_mul_cancel this, sub_add_add_cancel, hc,
  Int.emod_add_ediv']
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)
this : x ∣ abs x
⊢ c - abs x + (a + abs x) / x * x = a
no goals