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 : ℚ
x✝ : p - q ≃ 0
⊢ p ≃ q
no goals