lax_exact h.almost_smul_interchange m n 1 <;> rw [zsmul_int_one]
G : Type ?u.71849
inst✝ : AddCommGroup G
f✝ : G → ℤ
bound✝ : ℕ
h✝ : AlmostAdditive f✝ bound✝
m✝ n✝ : ℤ
g : G
f : ℤ → ℤ
bound : ℕ
h : AlmostAdditive f bound
m n : ℤ
⊢ |n * f m - m * f n| ≤ bound * (|m| + |n| + 2)
no goals