calc f n' ≥ n' - ↑((m + 3) * bound)
              := positive_linear_growth_of_large_enough_value h_a h n'
        _ ≥ ↑(R.toNat + (m + 3) * bound) - ↑((m + 3) * bound)
              := Int.sub_le_sub_right (c := _) <| Int.ofNat_le.mpr h_ge
        _ ≥ R.toNat := by custom_zify; linarith
        _ ≥ R       := Int.self_le_toNat ..
G : Type ?u.65059
f : AlmostHom ℤ
h✝ : ¬Function.BddAboveOn f.toFun (Set.Ici 0)
bound : ℕ
h_a : ∀ (g₁ g₂ : ℤ), |toFun f (g₁ + g₂) - toFun f g₁ - toFun f g₂| ≤ bound
m : ℕ
h : ↑bound * 2 < toFun f ↑m
R n : ℤ
n' : ℕ := Int.toNat n
h_ge✝ : ↑n' ≥ ↑(Int.toNat R + (m + 3) * bound)
this : ↑n' = n
h_ge : n' ≥ Int.toNat R + (m + 3) * bound := Iff.mp Int.ofNat_le h_ge✝
⊢ toFun f ↑n' ≥ R
no goals