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