exact ⟨_, by
  intro n
  have hypcomm := AlmostAdditive.almost_smul_interchange (hf₁) (f₂ n) n 1
  specialize hlin n
  simp only [smul_eq_mul, mul_one] at hypcomm
  calc |n * (f₁.comp f₂ n) - f₂ n * f₁ n|
      ≤ b₁*(|f₂ n| + |n| + 2) := hypcomm
    _ ≤ b₁*(a'*|n| + b' + |n| + 2) :=
        by apply mul_le_mul_of_nonneg_left
            (by simp only [add_le_add_iff_right, hlin]) (zero_le _)
    _ = b₁*(|n| * (a' + 1) + (b'+ 2)) := by ring
    _ ≤ b₁*(|n| * (a' + 1) + (b'+ 2)) + b₁*(a'+1) :=
        by simp only [le_add_iff_nonneg_right, zero_le]
    _ ≤ b₁*(|n| * (a' + 1) + (b'+ 2)) + b₁*(a'+1) + b₁*(|n|)*(b'+2) :=
        by simp only [le_add_iff_nonneg_right, zero_le]
    _ = (|n|+1)*(b₁*(a'+1 + b'+2)) := by ring⟩
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₁
⊢ ∃ k, ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * k
no goals