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

State before:
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
⊢ toFun f g ≥ -bound - ↑bound'
Tactic:
have : f (-g) - -f g ≥ -bound' := Int.neg_le_self_of_natAbs_le (hₐ g)
State after:
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'

State before:
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'
Tactic:
linarith [this, h (neg_nonpos_of_nonneg h_g)]
State after:
no goals