case negSucc.succ m hᵢ =>
  conv => lhs; rewrite [←Int.negSucc_sub_one]
  rewrite [sub_zsmul, one_zsmul, sub_mul, one_mul]
  calc |f (Int.negSucc m • g + -g) - (Int.negSucc m * f g - f g)|
      = |(-(f (Int.negSucc m • g) - f (Int.negSucc m • g + -g) - f g))
         + (f (Int.negSucc m • g) - Int.negSucc m * f g)|
          := congrArg Int.natAbs <| by linarith
    _ ≤ |f (Int.negSucc m • g) - f (Int.negSucc m • g + -g) - f g|
        + |f (Int.negSucc m • g) - Int.negSucc m * f g|
          := by conv => rhs; arg 1; rewrite [←Int.natAbs_neg]
                apply Int.natAbs_add_le
    _ ≤ bound + bound * (|Int.negSucc m| + 1)
          := Nat.add_le_add (by rewrite [←congrArg f <| neg_add_cancel_right ..]
                                apply h.almost_additive _ g)
                            hᵢ
    _ = bound * (|Int.negSucc m.succ| + 1)
          := by simp only [Int.natAbs_negSucc]; linarith
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
m : ℕ
hᵢ : |f (Int.negSucc m • g) - Int.negSucc m * f g| ≤ bound * (|Int.negSucc m| + 1)
⊢ |f (Int.negSucc (Nat.succ m) • g) - Int.negSucc (Nat.succ m) * f g| ≤ bound * (|Int.negSucc (Nat.succ m)| + 1)
no goals