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