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