calc |f₁.comp f₂ n - f₂.comp f₁ n|
  ≤ 2*(k₁ + k₂) := le_of_mul_le_mul_left goal_mul_n
    <| Or.resolve_left (Nat.eq_zero_or_pos ..) (Int.natAbs_ne_zero.2 c)
_ ≤ _ := self_le_add_left  (2*(k₁ + k₂)) |(f₁.comp f₂ - f₂.comp f₁) 0|
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
goal_mul_n : |n| * |toFun (AlmostHom.comp f₁ f₂) n - toFun (AlmostHom.comp f₂ f₁) n| ≤ |n| * (2 * (k₁ + k₂))
⊢ |toFun (AlmostHom.comp f₁ f₂) n - toFun (AlmostHom.comp f₂ f₁) n| ≤
    |toFun (AlmostHom.comp f₁ f₂ - AlmostHom.comp f₂ f₁) 0| + 2 * (k₁ + k₂)
no goals