let ⟨a', b', hlin⟩ := linear_growth_upper_bound_int f₂
G : Type ?u.41105
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
⊢ ∃ k, ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * k
G : Type ?u.41105
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
a' b' : ℕ
hlin : ∀ (n : ℤ), |toFun f₂ n| ≤ a' * |n| + b'
⊢ ∃ k, ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * k