calc
  b - a₁    ≃ _ := sub_defn
  b + (-a₁) ≃ _ := AA.substR (AA.subst₁ ‹a₁ ≃ a₂›)
  b + (-a₂) ≃ _ := Rel.symm sub_defn
  b - a₂    ≃ _ := Rel.refl
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
inst✝ : Subtraction ℤ
a₁ a₂ b : ℤ
x✝ : a₁ ≃ a₂
⊢ b - a₁ ≃ b - a₂
no goals