have succ_le_two_mul (a : ℕ) (ha : a ≠ 0) : a+1 ≤ 2*a := by
  cases a
  case zero => contradiction
  case succ => apply Nat.succ_le.2; linarith [NeZero.pos]
G : Type ?u.46675
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
⊢ Bounded (-AlmostHom.comp f₁ f₂ + AlmostHom.comp f₂ f₁)
G : Type ?u.46675
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
succ_le_two_mul : ∀ (a : ℕ), a ≠ 0 → a + 1 ≤ 2 * a
⊢ Bounded (-AlmostHom.comp f₁ f₂ + AlmostHom.comp f₂ f₁)