rewrite [←h_fm_nonneg, show (_:ℤ) * (m:ℤ) = (_:ℤ) • (m:ℤ) from rfl]
G : Type ?u.55607
f : ℤ → ℤ
bound : ℕ
h_bound : AlmostAdditive f bound
m : ℕ
h : f ↑m > ↑bound * 2
h_fm_nonneg : ↑(|f ↑m|) = f ↑m
n : ℕ
⊢ ↑(|f (↑n * ↑m)|) ≥ (f ↑m - ↑bound) * ↑(|↑n|) - ↑bound
G : Type ?u.55607
f : ℤ → ℤ
bound : ℕ
h_bound : AlmostAdditive f bound
m : ℕ
h : f ↑m > ↑bound * 2
h_fm_nonneg : ↑(|f ↑m|) = f ↑m
n : ℕ
⊢ ↑(|f (↑n • ↑m)|) ≥ (↑(|f ↑m|) - ↑bound) * ↑(|↑n|) - ↑bound