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