Theorem: Bounded.Bounded.almost_additive (RealsQuasiMorphisms/Basic.lean)

State before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : Bounded f bound
g₁ g₂ : G
⊢ |f (g₁ + g₂)| + |-f g₁| + |-f g₂| ≤ bound * 3
Tactic:
linarith [(f g₁).natAbs_neg, (f g₂).natAbs_neg,
          h (g₁ + g₂), h g₁, h g₂]
State after:
no goals