have reduce {x y : ℤ} : -x + (x + y) ≃ y := calc
  _ = -x + (x + y) := rfl
  _ ≃ (-x + x) + y := Rel.symm AA.assoc
  _ ≃ 0 + y        := AA.substL AA.inverseL
  _ ≃ y            := AA.identL
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a b₁ b₂ : ℤ
x✝ : a + b₁ ≃ a + b₂
⊢ b₁ ≃ b₂
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a b₁ b₂ : ℤ
x✝ : a + b₁ ≃ a + b₂
reduce : ∀ {x y : ℤ}, -x + (x + y) ≃ y
⊢ b₁ ≃ b₂