calc |f g| * |n|
  = |n * f g|                       := by rw [Nat.mul_comm, Int.natAbs_mul]
_ ≤ |n * f g - f (n • g)| + |f (n • g)|
      := by lax_exact Int.natAbs_add_le (n * f g - f (n • g)) (f (n • g)); linarith
_ = |f (n • g) - n * f g| + |f (n • g)|
      := by congr 1; rewrite [←Int.natAbs_neg]
            congr 1; linarith
_ ≤ bound * (|n| + 1) + |f (n • g)| := by linarith [h.almost_smul n g]
case h
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
m n : ℤ
g : G
⊢ |f g| * |n| ≤ bound * Nat.succ |n| + |f (n • g)|
no goals