show (p₁n * qd + p₁d * qn) * (p₂d * qd) ≃ (p₂n * qd + p₂d * qn) * (p₁d * qd)
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₁n p₁d : ℤ
denominator_positive✝² : Logic.AP (Positive p₁d)
p₂n p₂d : ℤ
denominator_positive✝¹ : Logic.AP (Positive p₂d)
qn qd : ℤ
denominator_positive✝ : Logic.AP (Positive qd)
x✝ : p₁n//p₁d ≃ p₂n//p₂d
⊢ (p₁n * qd + p₁d * qn)//(p₁d * qd) ≃ (p₂n * qd + p₂d * qn)//(p₂d * qd)
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₁n p₁d : ℤ
denominator_positive✝² : Logic.AP (Positive p₁d)
p₂n p₂d : ℤ
denominator_positive✝¹ : Logic.AP (Positive p₂d)
qn qd : ℤ
denominator_positive✝ : Logic.AP (Positive qd)
x✝ : p₁n//p₁d ≃ p₂n//p₂d
⊢ (p₁n * qd + p₁d * qn) * (p₂d * qd) ≃ (p₂n * qd + p₂d * qn) * (p₁d * qd)