induction m
case negSucc
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
m : ℕ
⊢ |f (Int.negSucc m • g) - Int.negSucc m * f g| ≤ bound * (|Int.negSucc m| + 1)
case negSucc.zero
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
⊢ |f (Int.negSucc Nat.zero • g) - Int.negSucc Nat.zero * f g| ≤ bound * (|Int.negSucc Nat.zero| + 1)

case negSucc.succ
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
n✝ : ℕ
n_ih✝ : |f (Int.negSucc n✝ • g) - Int.negSucc n✝ * f g| ≤ bound * (|Int.negSucc n✝| + 1)
⊢ |f (Int.negSucc (Nat.succ n✝) • g) - Int.negSucc (Nat.succ n✝) * f g| ≤ bound * (|Int.negSucc (Nat.succ n✝)| + 1)