Theorem: AlmostAdditive.almost_zero (RealsQuasiMorphisms/Basic.lean)

State before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
m n : ℤ
g : G
⊢ |f 0| = |f (0 + 0) - f 0 - f 0|
Tactic:
rw [←Int.natAbs_neg, add_zero,
    sub_self, zero_sub]
State after:
no goals