rw [zsmul_int_one]
case e_a.e_m.e_a
G : Type ?u.87514
inst✝ : AddCommGroup G
f✝ : G → ℤ
bound✝ : ℕ
h✝ : AlmostAdditive f✝ bound✝
m n✝ : ℤ
g : G
f : ℤ → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
⊢ n = n • 1
no goals