calc
  p * q₁ ≃ _ := mul_comm
  q₁ * p ≃ _ := mul_substL ‹q₁ ≃ q₂›
  q₂ * p ≃ _ := mul_comm
  p * q₂ ≃ _ := eqv_refl
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p q₁ q₂ : Fraction ℤ
x✝ : q₁ ≃ q₂
⊢ p * q₁ ≃ p * q₂
no goals