rw [neg_add_rev, neg_neg, sub_eq_neg_add]
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 : ℤ
⊢ -(-toFun (AlmostHom.comp f₁ f₂) n + toFun (AlmostHom.comp f₂ f₁) n) =
    toFun (AlmostHom.comp f₁ f₂) n - toFun (AlmostHom.comp f₂ f₁) n
no goals