linarith [(f g₁).natAbs_neg, (f g₂).natAbs_neg,
          h (g₁ + g₂), h g₁, h g₂]
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
no goals