lax_exact h.linear_growth_upper_bound n 1
G : Type ?u.78830
inst✝ : AddCommGroup G
f✝ : G → ℤ
bound✝ : ℕ
h✝ : AlmostAdditive f✝ bound✝
m n✝ : ℤ
g : G
f : ℤ → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
⊢ |f n| ≤ (bound + |f 1|) * |n| + bound
case e_a.e_m.e_a
G : Type ?u.78830
inst✝ : AddCommGroup G
f✝ : G → ℤ
bound✝ : ℕ
h✝ : AlmostAdditive f✝ bound✝
m n✝ : ℤ
g : G
f : ℤ → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
⊢ n = n • 1