calc
  q / p₁   ≃ _ := div_mul_recip
  q * p₁⁻¹ ≃ _ := mul_substR (recip_subst ‹p₁ ≃ p₂›)
  q * p₂⁻¹ ≃ _ := eqv_symm div_mul_recip
  q / p₂   ≃ _ := eqv_refl
ℕ ℤ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
ℚ : Type
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
p₁ p₂ q : ℚ
inst✝¹ : AP (p₁ ≄ 0)
inst✝ : AP (p₂ ≄ 0)
x✝ : p₁ ≃ p₂
⊢ q / p₁ ≃ q / p₂
no goals