conv => lhs; rewrite [←Int.negSucc_sub_one]
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)
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 - 1) • g) - (Int.negSucc m - 1) * f g| ≤ bound * (|Int.negSucc (Nat.succ m)| + 1)