linarith [h.almost_smul n g]
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
m n : ℤ
g : G
⊢ |f (n • g) - n * f g| + |f (n • g)| ≤ bound * (|n| + 1) + |f (n • g)|
no goals