no goals
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : CommRing α
a b : α
u₁ u₂ : αˣ
⊢ a /ₚ u₁ - b /ₚ u₂ = (a * ↑u₂ - ↑u₁ * b) /ₚ (u₁ * u₂)
simp only [sub_eq_add_neg, neg_divp, divp_add_divp, mul_neg]