linarith [h.almost_additive (-g) g, h.almost_zero]
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
m n : ℤ
g : G
⊢ |f (-g + g) - f (-g) - f g| + |f 0| ≤ bound * 2
no goals