let ⟨k₁, hf₁⟩ := comp_almost_mul f₁ f₂
G : Type ?u.46675
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
succ_le_two_mul : ∀ (a : ℕ), a ≠ 0 → a + 1 ≤ 2 * a
⊢ ∃ bound, ∀ (g : ℤ), |toFun (-AlmostHom.comp f₁ f₂ + AlmostHom.comp f₂ f₁) g| ≤ bound
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₁
⊢ ∃ bound, ∀ (g : ℤ), |toFun (-AlmostHom.comp f₁ f₂ + AlmostHom.comp f₂ f₁) g| ≤ bound