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

State before:
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)
Tactic:
lax_exact h.almost_smul_interchange m n 1 <;> rw [zsmul_int_one]
State after:
no goals