rw [Nat.add_comm, Nat.add_assoc, Nat.mul_two]
G : Type u_1
inst✝ : AddCommGroup G
f : ℤ → ℤ
bound : ℕ
h : AlmostAdditive f bound
f₁ f₂ : G → ℤ
bound' : ℕ
h' : Bounded (-f₁ + f₂) bound'
g : G
⊢ bound + ((bound + |f 1|) * bound' + bound) = (bound + |f 1|) * bound' + bound * 2
no goals