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 m • g + -g) - (Int.negSucc m * f g - f g)| ≤ bound * (|Int.negSucc (Nat.succ m)| + 1)
no goals