linarith [h_comp]
G : Type ?u.74532
f : AlmostHom ℤ
h✝ : ¬Function.BddAboveOn f.toFun (Set.Ici 0)
N : ℕ
h : ∀ (n : ℤ), n ≥ ↑N → toFun f n ≥ 0
a b : ℕ
h' : ∀ (n : ℤ), |toFun f n| ≤ a * |n| + b
n : ℤ
h_nonneg : n ≥ 0
h_comp : ¬n ≥ ↑N
⊢ n ≤ ↑N
no goals