calc
  _ ≃ p/q     := eqv_refl
  _ ≃ p * q⁻¹ := div_mul_recip
  _ ≃ 0 * q⁻¹ := mul_substL ‹p ≃ 0›
  _ ≃ 0       := mul_absorbL
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Subtraction ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Sign ℚ
p q : ℚ
inst✝ : AP (q ≄ 0)
x✝ : p ≃ 0
⊢ p / q ≃ 0
no goals