linarith [this, h (-n) (Int.le_neg_of_le_neg h_le)]
G : Type ?u.72001
f : AlmostHom ℤ
h✝ : ¬Function.BddAboveOn f.toFun (Set.Ici 0)
R : ℤ
bound : ℕ
h_a : ∀ (g : ℤ), |toFun f (-g) - -toFun f g| ≤ bound
N : ℕ
h : ∀ (n : ℤ), n ≥ ↑N → toFun f n ≥ -R + ↑bound
n : ℤ
h_le : n ≤ -↑N
this : toFun f n - -toFun f (-n) ≤ ↑bound
⊢ toFun f n ≤ R
no goals