rw [Int.add_sub_cancel_right (f₁ g) (f₂ g),
    ←Int.sub_eq_neg_add, Int.sub_add_cancel]
G : Type u_1
inst✝ : AddCommGroup G
f : ℤ → ℤ
bound : ℕ
h : AlmostAdditive f bound
f₁ f₂ : G → ℤ
bound' : ℕ
h' : Bounded (-f₁ + f₂) bound'
g : G
⊢ -f (f₁ g) + f (f₂ g) = f (f₁ g + (f₂ g - f₁ g)) - f (f₁ g) - f (f₂ g - f₁ g) + f (f₂ g - f₁ g)
no goals