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