apply Int.le_trans (Int.subNatNat_le_sub ..)
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)|) ≥ Int.subNatNat ((|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 ↑m| - bound) * n - bound) ≤ ↑(|f (n • ↑m)|)