Theorem: AlmostHom.nonneg_total_integers (RealsQuasiMorphisms/Order.lean)

State before:
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
Tactic:
linarith [h_comp]
State after:
no goals