linarith [this, h (neg_nonpos_of_nonneg 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 : Function.BddAboveOnBy f.toFun (Set.Iic 0) bound
g : G
h_g : g ≥ 0
this : toFun f (-g) - -toFun f g ≥ -↑bound'
⊢ toFun f g ≥ -bound - ↑bound'
no goals