rewrite [QuotientAddGroup.leftRel_apply]
G : Type ?u.57147
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
⊢ Setoid.r (AlmostHom.comp f₁ f₂) (AlmostHom.comp f₂ f₁)
G : Type ?u.57147
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
⊢ -AlmostHom.comp f₁ f₂ + AlmostHom.comp f₂ f₁ ∈ boundedAlmostHoms ℤ