case mp =>
  intro (_ : a - b ≃ 0)
  show a ≃ b
  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 : ℤ
⊢ a - b ≃ 0 → a ≃ b
no goals