case mpr =>
  intro (_ : p ≃ 0)
  show p/q ≃ 0
  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)
⊢ p ≃ 0 → p / q ≃ 0
no goals