have : ↑n' = n :=
  Int.toNat_of_nonneg <| Int.le_trans (Int.ofNat_zero_le ..) h_ge
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 : ℤ
h_ge : n ≥ ↑(Int.toNat R + (m + 3) * bound)
n' : ℕ := Int.toNat n
⊢ toFun f n ≥ R
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 : ℤ
h_ge : n ≥ ↑(Int.toNat R + (m + 3) * bound)
n' : ℕ := Int.toNat n
this : ↑n' = n
⊢ toFun f n ≥ R