rewrite [Nat.succ_eq_add_one, Nat.cast_succ]
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
m : ℕ
hᵢ : |f (m • g) - ↑m * f g| ≤ bound * (|↑m| + 1)
⊢ ↑(Nat.succ m) * f g = f g + ↑m * f g
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
m : ℕ
hᵢ : |f (m • g) - ↑m * f g| ≤ bound * (|↑m| + 1)
⊢ (↑m + 1) * f g = f g + ↑m * f g