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