calc
  p₁ / q   ≃ _ := div_mul_recip
  p₁ * q⁻¹ ≃ _ := mul_substL ‹p₁ ≃ p₂›
  p₂ * q⁻¹ ≃ _ := eqv_symm div_mul_recip
  p₂ / q   ≃ _ := 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 (q ≄ 0)
x✝ : p₁ ≃ p₂
⊢ p₁ / q ≃ p₂ / q
no goals