linarith
G : Type u_1
inst✝ : AddCommGroup G
f₁ : ℤ → ℤ
bound₁ : ℕ
h₁ : AlmostAdditive f₁ bound₁
f₂ : G → ℤ
bound₂ : ℕ
h₂ : AlmostAdditive f₂ bound₂
x y : G
⊢ bound₁ + ((bound₁ + |f₁ 1|) * |f₂ (x + y) - f₂ x - f₂ y| + bound₁) + bound₁ =
    (bound₁ + |f₁ 1|) * |f₂ (x + y) - f₂ x - f₂ y| + bound₁ * 3
no goals