calc
  -p     ≃ _ := eqv_symm add_identL
  0 + -p ≃ _ := add_substL (eqv_symm ‹p ≃ 0›)
  p + -p ≃ _ := add_inverseR
  0      ≃ _ := eqv_refl
ℕ ℤ : Type
inst✝⁶ : Natural ℕ
inst✝⁵ : Integer ℤ
ℚ : Type
inst✝⁴ : Core ℚ
inst✝³ : Addition ℚ
inst✝² : Multiplication ℚ
inst✝¹ : Negation ℚ
inst✝ : Subtraction ℚ
p : ℚ
x✝ : p ≃ 0
⊢ -p ≃ 0
no goals