case mpr =>
  intro (_ : p ≃ q)
  show p - q ≃ 0
  calc
    p - q  ≃ _ := sub_add_neg
    p + -q ≃ _ := add_substL ‹p ≃ q›
    q + -q ≃ _ := add_inverseR
    0      ≃ _ := eqv_refl
ℕ ℤ : Type
inst✝⁶ : Natural ℕ
inst✝⁵ : Integer ℤ
ℚ : Type
inst✝⁴ : Core ℚ
inst✝³ : Addition ℚ
inst✝² : Multiplication ℚ
inst✝¹ : Negation ℚ
inst✝ : Subtraction ℚ
p q : ℚ
⊢ p ≃ q → p - q ≃ 0
no goals