rewrite [←Int.natAbs_neg, ←add_left_neg g]
case e_a
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
m n : ℤ
g : G
⊢ |f (-g) + f g - f 0| = |f (-g + g) - f (-g) - f g|
case e_a
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
m n : ℤ
g : G
⊢ |-(f (-g) + f g - f (-g + g))| = |f (-g + g) - f (-g) - f g|