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