simp only [le_add_iff_nonneg_right, zero_le]
G : Type ?u.41105
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
a' b' : ℕ
hlin✝ : ∀ (n : ℤ), |toFun f₂ n| ≤ a' * |n| + b'
b₁ : ℕ
hf₁ : AlmostAdditive f₁.toFun b₁
n : ℤ
hlin : |toFun f₂ n| ≤ a' * |n| + b'
hypcomm : |n * toFun f₁ (toFun f₂ n) - toFun f₂ n * toFun f₁ n| ≤ b₁ * (|toFun f₂ n| + |n| + 2)
⊢ b₁ * (|n| * (a' + 1) + (b' + 2)) ≤ b₁ * (|n| * (a' + 1) + (b' + 2)) + b₁ * (a' + 1)
no goals