linarith
case e_a.e_m
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))) = f (f₁ g + f₂ g) - f (f₁ g) - f (f₂ g)
no goals