have ofNat_two : ((2 : Nat) : Int) = 2 := rfl
case neg.refine'_2
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : ↑x.natAbs ≤ ↑(2 * c.natAbs)
⊢ ↑(2 * (c - |x|).natAbs) < ↑x.natAbs
case neg.refine'_2
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : ↑x.natAbs ≤ ↑(2 * c.natAbs)
ofNat_two : ↑2 = 2
⊢ ↑(2 * (c - |x|).natAbs) < ↑x.natAbs