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