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

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