exact_mod_cast h_bound.linear_growth_lower_bound n m
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 ↑m| - bound) * n - bound) ≤ ↑(|f (n • ↑m)|)
no goals