case mpr =>
  intro (_ : pn ≃ 0)
  show pn//pd ≃ 0
  show pn//pd ≃ 0//1
  show pn * 1 ≃ 0 * pd
  calc
    pn * 1 ≃ _ := AA.identR
    pn     ≃ _ := ‹pn ≃ 0›
    0      ≃ _ := Rel.symm AA.absorbL
    0 * pd ≃ _ := Rel.refl
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
⊢ (pn//pd).numerator ≃ 0 → pn//pd ≃ 0
no goals