show |(-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
⊢ |HAdd.hAdd (-f ∘ (f₁ + f₂)) (f ∘ f₁ + 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