simp
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
⊢ |f (Int.ofNat Nat.zero • g) - Int.ofNat Nat.zero * f g| ≤ bound * (|Int.ofNat Nat.zero| + 1)
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
⊢ |f 0| ≤ bound