rw [←mul_assoc, mul_comm |n|]
G : Type ?u.46675
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
succ_le_two_mul : ∀ (a : ℕ), a ≠ 0 → a + 1 ≤ 2 * a
k₁ : ℕ
hf₁ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * k₁
k₂ : ℕ
hf₂ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₂ f₁) n - toFun f₁ n * toFun f₂ n| ≤ (|n| + 1) * k₂
n : ℤ
triag :
  |n * toFun (AlmostHom.comp f₁ f₂) n - n * toFun (AlmostHom.comp f₂ f₁) n| ≤
    |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| +
      |toFun f₂ n * toFun f₁ n - n * toFun (AlmostHom.comp f₂ f₁) n|
c : ¬n = 0
⊢ (|n| + 1) * (k₁ + k₂) ≤ |n| * (2 * (k₁ + k₂))
G : Type ?u.46675
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
succ_le_two_mul : ∀ (a : ℕ), a ≠ 0 → a + 1 ≤ 2 * a
k₁ : ℕ
hf₁ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * k₁
k₂ : ℕ
hf₂ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₂ f₁) n - toFun f₁ n * toFun f₂ n| ≤ (|n| + 1) * k₂
n : ℤ
triag :
  |n * toFun (AlmostHom.comp f₁ f₂) n - n * toFun (AlmostHom.comp f₂ f₁) n| ≤
    |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| +
      |toFun f₂ n * toFun f₁ n - n * toFun (AlmostHom.comp f₂ f₁) n|
c : ¬n = 0
⊢ (|n| + 1) * (k₁ + k₂) ≤ 2 * |n| * (k₁ + k₂)