let ⟨m, h_nonneg, h⟩ := h (bound * 2)
G : Type ?u.65059
f : AlmostHom ℤ
bound : ℕ
h_a : ∀ (g₁ g₂ : ℤ), |toFun f (g₁ + g₂) - toFun f g₁ - toFun f g₂| ≤ bound
h : ∀ (b : ℤ), Exists fun {a} => a ∈ Set.Ici 0 ∧ b < toFun f a
⊢ ∃ m, ↑bound * 2 < toFun f ↑m
G : Type ?u.65059
f : AlmostHom ℤ
bound : ℕ
h_a : ∀ (g₁ g₂ : ℤ), |toFun f (g₁ + g₂) - toFun f g₁ - toFun f g₂| ≤ bound
h✝ : ∀ (b : ℤ), Exists fun {a} => a ∈ Set.Ici 0 ∧ b < toFun f a
m : ℤ
h_nonneg : m ∈ Set.Ici 0
h : ↑bound * 2 < toFun f m
⊢ ∃ m, ↑bound * 2 < toFun f ↑m