rewrite [tsub_mul, Nat.sub_sub, ←Nat.mul_succ]
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
m n : ℤ
g : G
⊢ (|f g| - bound) * |n| - bound ≤ |f (n • g)|
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
m n : ℤ
g : G
⊢ |f g| * |n| - bound * Nat.succ |n| ≤ |f (n • g)|