rewrite [Int.abs_eq_natAbs,
         Int.subNatNat_of_le <|
           show bound ≤ |f m| from Int.ofNat_le.mp <|
           calc (bound:ℤ) ≤ bound * 2 := by linarith
                        _ ≤ f m       := Int.le_of_lt h
                        _ ≤ |f m|     := Int.le_natAbs]
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 : ℕ
⊢ abs (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 (n • ↑m)|) ≥ ↑(|f ↑m| - bound) * ↑n - ↑bound