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