rewrite [←Int.natAbs_neg]
G : Type u_1
inst✝ : AddCommGroup G
f : ℤ → ℤ
bound : ℕ
h : AlmostAdditive f bound
f₁ f₂ : G → ℤ
g : G
⊢ |-f (f₁ g + f₂ g) + (f (f₁ g) + f (f₂ g))| ≤ bound
G : Type u_1
inst✝ : AddCommGroup G
f : ℤ → ℤ
bound : ℕ
h : AlmostAdditive f bound
f₁ f₂ : G → ℤ
g : G
⊢ |-(-f (f₁ g + f₂ g) + (f (f₁ g) + f (f₂ g)))| ≤ bound