linarith [this, h (neg_nonneg_of_nonpos h_g)]
G : Type u_1
inst✝ : OrderedAddCommGroup G
f : AlmostHom G
bound' : ℕ
hₐ : ∀ (g : G), |toFun f (-g) - -toFun f g| ≤ bound'
bound : ℤ
h : ∀ {g : G}, g ≥ 0 → toFun f g ≥ bound
g : G
h_g : g ∈ Set.Iic 0
this : toFun f g - -toFun f (-g) ≤ ↑bound'
⊢ toFun f g ≤ ↑bound' - bound
no goals